YES 2.378 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ LR

mainModule List
  ((intersect :: (Eq a, Eq b) => [Either b a]  ->  [Either b a]  ->  [Either b a]) :: (Eq a, Eq b) => [Either b a]  ->  [Either b a]  ->  [Either b a])

module List where
  import qualified Maybe
import qualified Prelude
  intersect :: Eq a => [a]  ->  [a]  ->  [a]
intersect = intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [a]  ->  [a]
intersectBy eq xs ys = concatMap (\vv2 ->
case vv2 of
  x->  if any (eq x) ys then x : [] else []
  _-> []
) xs


module Maybe where
  import qualified List
import qualified Prelude


Lambda Reductions:
The following Lambda expression
\vv2→
case vv2 of
 x → if any (eq x) ys then x : [] else []
 _ → []

is transformed to
intersectBy0 eq ys vv2 = 
case vv2 of
 x → if any (eq x) ys then x : [] else []
 _ → []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR

mainModule List
  ((intersect :: (Eq b, Eq a) => [Either b a]  ->  [Either b a]  ->  [Either b a]) :: (Eq a, Eq b) => [Either b a]  ->  [Either b a]  ->  [Either b a])

module List where
  import qualified Maybe
import qualified Prelude
  intersect :: Eq a => [a]  ->  [a]  ->  [a]
intersect = intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [a]  ->  [a]
intersectBy eq xs ys = concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 = 
case vv2 of
  x->  if any (eq x) ys then x : [] else []
  _-> []


module Maybe where
  import qualified List
import qualified Prelude


Case Reductions:
The following Case expression
case vv2 of
 x → if any (eq x) ys then x : [] else []
 _ → []

is transformed to
intersectBy00 eq ys x = if any (eq x) ys then x : [] else []
intersectBy00 eq ys _ = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR

mainModule List
  ((intersect :: (Eq a, Eq b) => [Either b a]  ->  [Either b a]  ->  [Either b a]) :: (Eq a, Eq b) => [Either b a]  ->  [Either b a]  ->  [Either b a])

module List where
  import qualified Maybe
import qualified Prelude
  intersect :: Eq a => [a]  ->  [a]  ->  [a]
intersect = intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [a]  ->  [a]
intersectBy eq xs ys = concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 = intersectBy00 eq ys vv2

  
intersectBy00 eq ys x =  if any (eq x) ys then x : [] else []
intersectBy00 eq ys _ = []


module Maybe where
  import qualified List
import qualified Prelude


If Reductions:
The following If expression
if any (eq x) ys then x : [] else []

is transformed to
intersectBy000 x True = x : []
intersectBy000 x False = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR

mainModule List
  ((intersect :: (Eq b, Eq a) => [Either b a]  ->  [Either b a]  ->  [Either b a]) :: (Eq b, Eq a) => [Either b a]  ->  [Either b a]  ->  [Either b a])

module List where
  import qualified Maybe
import qualified Prelude
  intersect :: Eq a => [a]  ->  [a]  ->  [a]
intersect = intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [a]  ->  [a]
intersectBy eq xs ys = concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 = intersectBy00 eq ys vv2

  
intersectBy00 eq ys x = intersectBy000 x (any (eq x) ys)
intersectBy00 eq ys _ = []

  
intersectBy000 x True = x : []
intersectBy000 x False = []


module Maybe where
  import qualified List
import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR

mainModule List
  ((intersect :: (Eq a, Eq b) => [Either b a]  ->  [Either b a]  ->  [Either b a]) :: (Eq b, Eq a) => [Either b a]  ->  [Either b a]  ->  [Either b a])

module List where
  import qualified Maybe
import qualified Prelude
  intersect :: Eq a => [a]  ->  [a]  ->  [a]
intersect = intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [a]  ->  [a]
intersectBy eq xs ys = concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 = intersectBy00 eq ys vv2

  
intersectBy00 eq ys x = intersectBy000 x (any (eq x) ys)
intersectBy00 eq ys vw = []

  
intersectBy000 x True = x : []
intersectBy000 x False = []


module Maybe where
  import qualified List
import qualified Prelude


Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow

mainModule List
  (intersect :: (Eq b, Eq a) => [Either b a]  ->  [Either b a]  ->  [Either b a])

module List where
  import qualified Maybe
import qualified Prelude
  intersect :: Eq a => [a]  ->  [a]  ->  [a]
intersect = intersectBy (==)

  intersectBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [a]  ->  [a]
intersectBy eq xs ys = concatMap (intersectBy0 eq ys) xs

  
intersectBy0 eq ys vv2 = intersectBy00 eq ys vv2

  
intersectBy00 eq ys x = intersectBy000 x (any (eq x) ys)
intersectBy00 eq ys vw = []

  
intersectBy000 x True = x : []
intersectBy000 x False = []


module Maybe where
  import qualified List
import qualified Prelude


Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xx3700), Succ(xx4001000)) → new_primPlusNat(xx3700, xx4001000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xx300100), Succ(xx400100)) → new_primMulNat(xx300100, Succ(xx400100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xx30000), Succ(xx40000)) → new_primEqNat(xx30000, xx40000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ QDPSizeChangeProof
                          ↳ QDP
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs(@2(xx3000, xx3001), @2(xx4000, xx4001), app(app(ty_@2, cc), cd), ce) → new_esEs(xx3000, xx4000, cc, cd)
new_esEs(@2(xx3000, xx3001), @2(xx4000, xx4001), app(ty_[], cf), ce) → new_esEs0(xx3000, xx4000, cf)
new_esEs3(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), baf, bag, app(ty_[], bbb)) → new_esEs0(xx3002, xx4002, bbb)
new_esEs3(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), baf, bag, app(app(ty_@2, bah), bba)) → new_esEs(xx3002, xx4002, bah, bba)
new_esEs3(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(app(ty_Either, bdg), bdh), bag, bcc) → new_esEs2(xx3000, xx4000, bdg, bdh)
new_esEs3(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), baf, bag, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs3(xx3002, xx4002, bbf, bbg, bbh)
new_esEs3(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), baf, app(app(ty_@2, bca), bcb), bcc) → new_esEs(xx3001, xx4001, bca, bcb)
new_esEs3(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), baf, app(ty_[], bcd), bcc) → new_esEs0(xx3001, xx4001, bcd)
new_esEs3(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), baf, bag, app(ty_Maybe, bbc)) → new_esEs1(xx3002, xx4002, bbc)
new_esEs3(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(app(ty_@2, bdc), bdd), bag, bcc) → new_esEs(xx3000, xx4000, bdc, bdd)
new_esEs1(Just(xx3000), Just(xx4000), app(app(ty_@2, eh), fa)) → new_esEs(xx3000, xx4000, eh, fa)
new_esEs3(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(ty_[], bde), bag, bcc) → new_esEs0(xx3000, xx4000, bde)
new_esEs3(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), baf, app(app(ty_Either, bcf), bcg), bcc) → new_esEs2(xx3001, xx4001, bcf, bcg)
new_esEs(@2(xx3000, xx3001), @2(xx4000, xx4001), ba, app(ty_Maybe, be)) → new_esEs1(xx3001, xx4001, be)
new_esEs1(Just(xx3000), Just(xx4000), app(app(app(ty_@3, fg), fh), ga)) → new_esEs3(xx3000, xx4000, fg, fh, ga)
new_esEs1(Just(xx3000), Just(xx4000), app(ty_[], fb)) → new_esEs0(xx3000, xx4000, fb)
new_esEs2(Left(xx3000), Left(xx4000), app(app(ty_Either, gg), gh), gd) → new_esEs2(xx3000, xx4000, gg, gh)
new_esEs2(Left(xx3000), Left(xx4000), app(app(app(ty_@3, ha), hb), hc), gd) → new_esEs3(xx3000, xx4000, ha, hb, hc)
new_esEs3(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(ty_Maybe, bdf), bag, bcc) → new_esEs1(xx3000, xx4000, bdf)
new_esEs2(Left(xx3000), Left(xx4000), app(ty_Maybe, gf), gd) → new_esEs1(xx3000, xx4000, gf)
new_esEs1(Just(xx3000), Just(xx4000), app(app(ty_Either, fd), ff)) → new_esEs2(xx3000, xx4000, fd, ff)
new_esEs3(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), baf, bag, app(app(ty_Either, bbd), bbe)) → new_esEs2(xx3002, xx4002, bbd, bbe)
new_esEs3(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), baf, app(app(app(ty_@3, bch), bda), bdb), bcc) → new_esEs3(xx3001, xx4001, bch, bda, bdb)
new_esEs0(:(xx3000, xx3001), :(xx4000, xx4001), app(ty_Maybe, eb)) → new_esEs1(xx3000, xx4000, eb)
new_esEs0(:(xx3000, xx3001), :(xx4000, xx4001), app(app(ty_Either, ec), ed)) → new_esEs2(xx3000, xx4000, ec, ed)
new_esEs(@2(xx3000, xx3001), @2(xx4000, xx4001), ba, app(app(ty_Either, bf), bg)) → new_esEs2(xx3001, xx4001, bf, bg)
new_esEs(@2(xx3000, xx3001), @2(xx4000, xx4001), ba, app(app(app(ty_@3, bh), ca), cb)) → new_esEs3(xx3001, xx4001, bh, ca, cb)
new_esEs2(Right(xx3000), Right(xx4000), hd, app(app(ty_@2, he), hf)) → new_esEs(xx3000, xx4000, he, hf)
new_esEs2(Right(xx3000), Right(xx4000), hd, app(ty_[], hg)) → new_esEs0(xx3000, xx4000, hg)
new_esEs2(Right(xx3000), Right(xx4000), hd, app(app(ty_Either, baa), bab)) → new_esEs2(xx3000, xx4000, baa, bab)
new_esEs(@2(xx3000, xx3001), @2(xx4000, xx4001), ba, app(ty_[], bd)) → new_esEs0(xx3001, xx4001, bd)
new_esEs1(Just(xx3000), Just(xx4000), app(ty_Maybe, fc)) → new_esEs1(xx3000, xx4000, fc)
new_esEs2(Right(xx3000), Right(xx4000), hd, app(ty_Maybe, hh)) → new_esEs1(xx3000, xx4000, hh)
new_esEs0(:(xx3000, xx3001), :(xx4000, xx4001), app(app(app(ty_@3, ee), ef), eg)) → new_esEs3(xx3000, xx4000, ee, ef, eg)
new_esEs2(Left(xx3000), Left(xx4000), app(app(ty_@2, gb), gc), gd) → new_esEs(xx3000, xx4000, gb, gc)
new_esEs(@2(xx3000, xx3001), @2(xx4000, xx4001), ba, app(app(ty_@2, bb), bc)) → new_esEs(xx3001, xx4001, bb, bc)
new_esEs(@2(xx3000, xx3001), @2(xx4000, xx4001), app(app(ty_Either, da), db), ce) → new_esEs2(xx3000, xx4000, da, db)
new_esEs0(:(xx3000, xx3001), :(xx4000, xx4001), app(app(ty_@2, dg), dh)) → new_esEs(xx3000, xx4000, dg, dh)
new_esEs0(:(xx3000, xx3001), :(xx4000, xx4001), app(ty_[], ea)) → new_esEs0(xx3000, xx4000, ea)
new_esEs(@2(xx3000, xx3001), @2(xx4000, xx4001), app(app(app(ty_@3, dc), dd), de), ce) → new_esEs3(xx3000, xx4000, dc, dd, de)
new_esEs2(Left(xx3000), Left(xx4000), app(ty_[], ge), gd) → new_esEs0(xx3000, xx4000, ge)
new_esEs2(Right(xx3000), Right(xx4000), hd, app(app(app(ty_@3, bac), bad), bae)) → new_esEs3(xx3000, xx4000, bac, bad, bae)
new_esEs0(:(xx3000, xx3001), :(xx4000, xx4001), df) → new_esEs0(xx3001, xx4001, df)
new_esEs3(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), app(app(app(ty_@3, bea), beb), bec), bag, bcc) → new_esEs3(xx3000, xx4000, bea, beb, bec)
new_esEs(@2(xx3000, xx3001), @2(xx4000, xx4001), app(ty_Maybe, cg), ce) → new_esEs1(xx3000, xx4000, cg)
new_esEs3(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), baf, app(ty_Maybe, bce), bcc) → new_esEs1(xx3001, xx4001, bce)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs0(Left(xx300), :(Right(xx400), xx41), xx5, bc, bd) → new_psPs(xx300, False, xx41, xx5, bc, bd)
new_psPs1(xx20, False, xx22, xx23, be, bf) → new_psPs0(Right(xx20), xx22, xx23, be, bf)
new_psPs0(Right(xx300), :(Left(xx400), xx41), xx5, bc, bd) → new_psPs1(xx300, False, xx41, xx5, bc, bd)
new_psPs(xx11, False, xx13, xx14, ba, bb) → new_psPs0(Left(xx11), xx13, xx14, ba, bb)
new_psPs0(Left(xx300), :(Left(xx400), xx41), xx5, bc, bd) → new_psPs(xx300, new_esEs4(xx300, xx400, bc), xx41, xx5, bc, bd)
new_psPs0(Right(xx300), :(Right(xx400), xx41), xx5, bc, bd) → new_psPs1(xx300, new_esEs5(xx300, xx400, bd), xx41, xx5, bc, bd)

The TRS R consists of the following rules:

new_esEs25(xx3001, xx4001, app(ty_[], bec)) → new_esEs14(xx3001, xx4001, bec)
new_esEs25(xx3001, xx4001, ty_Char) → new_esEs19(xx3001, xx4001)
new_esEs27(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs20(xx3001, xx4001, app(ty_Maybe, he)) → new_esEs17(xx3001, xx4001, he)
new_esEs27(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs25(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Bool) → new_esEs10(xx3000, xx4000)
new_primEqInt(Neg(Succ(xx30000)), Pos(xx4000)) → False
new_primEqInt(Pos(Succ(xx30000)), Neg(xx4000)) → False
new_esEs5(xx300, xx400, ty_Integer) → new_esEs12(xx300, xx400)
new_esEs16(:%(xx3000, xx3001), :%(xx4000, xx4001), gd) → new_asAs(new_esEs23(xx3000, xx4000, gd), new_esEs22(xx3001, xx4001, gd))
new_esEs26(xx3000, xx4000, app(ty_Ratio, bff)) → new_esEs16(xx3000, xx4000, bff)
new_primEqInt(Pos(Zero), Neg(Succ(xx40000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(xx40000))) → False
new_esEs6(Left(xx3000), Left(xx4000), ty_@0, bg) → new_esEs7(xx3000, xx4000)
new_esEs5(xx300, xx400, app(ty_[], eh)) → new_esEs14(xx300, xx400, eh)
new_esEs25(xx3001, xx4001, app(ty_Maybe, bee)) → new_esEs17(xx3001, xx4001, bee)
new_esEs24(xx3002, xx4002, app(ty_Maybe, bdc)) → new_esEs17(xx3002, xx4002, bdc)
new_esEs5(xx300, xx400, ty_@0) → new_esEs7(xx300, xx400)
new_esEs20(xx3001, xx4001, ty_Bool) → new_esEs10(xx3001, xx4001)
new_esEs8(GT, EQ) → False
new_esEs8(EQ, GT) → False
new_esEs20(xx3001, xx4001, ty_Char) → new_esEs19(xx3001, xx4001)
new_esEs24(xx3002, xx4002, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs18(xx3002, xx4002, bdf, bdg, bdh)
new_esEs17(Just(xx3000), Just(xx4000), app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs18(xx3000, xx4000, bcd, bce, bcf)
new_primMulNat0(Zero, Zero) → Zero
new_esEs27(xx3000, xx4000, app(ty_Ratio, bgh)) → new_esEs16(xx3000, xx4000, bgh)
new_esEs25(xx3001, xx4001, ty_Bool) → new_esEs10(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(app(ty_Either, bef), beg)) → new_esEs6(xx3001, xx4001, bef, beg)
new_esEs5(xx300, xx400, ty_Double) → new_esEs9(xx300, xx400)
new_esEs6(Left(xx3000), Left(xx4000), app(app(ty_Either, ce), cf), bg) → new_esEs6(xx3000, xx4000, ce, cf)
new_esEs4(xx300, xx400, ty_Ordering) → new_esEs8(xx300, xx400)
new_esEs5(xx300, xx400, app(app(ty_Either, fc), fd)) → new_esEs6(xx300, xx400, fc, fd)
new_esEs20(xx3001, xx4001, app(ty_Ratio, hd)) → new_esEs16(xx3001, xx4001, hd)
new_esEs24(xx3002, xx4002, ty_Double) → new_esEs9(xx3002, xx4002)
new_esEs17(Just(xx3000), Just(xx4000), ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_Ratio, cc), bg) → new_esEs16(xx3000, xx4000, cc)
new_esEs27(xx3000, xx4000, app(ty_Maybe, bha)) → new_esEs17(xx3000, xx4000, bha)
new_esEs26(xx3000, xx4000, app(app(app(ty_@3, bgb), bgc), bgd)) → new_esEs18(xx3000, xx4000, bgb, bgc, bgd)
new_esEs24(xx3002, xx4002, app(app(ty_Either, bdd), bde)) → new_esEs6(xx3002, xx4002, bdd, bde)
new_esEs27(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs24(xx3002, xx4002, app(app(ty_@2, bcg), bch)) → new_esEs13(xx3002, xx4002, bcg, bch)
new_esEs17(Just(xx3000), Just(xx4000), ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(ty_Maybe, bag)) → new_esEs17(xx3000, xx4000, bag)
new_esEs25(xx3001, xx4001, app(ty_Ratio, bed)) → new_esEs16(xx3001, xx4001, bed)
new_esEs24(xx3002, xx4002, app(ty_[], bda)) → new_esEs14(xx3002, xx4002, bda)
new_esEs26(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs5(xx300, xx400, ty_Float) → new_esEs11(xx300, xx400)
new_esEs24(xx3002, xx4002, ty_Integer) → new_esEs12(xx3002, xx4002)
new_sr(Pos(xx30010), Neg(xx40010)) → Neg(new_primMulNat0(xx30010, xx40010))
new_sr(Neg(xx30010), Pos(xx40010)) → Neg(new_primMulNat0(xx30010, xx40010))
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs20(xx3001, xx4001, ty_Float) → new_esEs11(xx3001, xx4001)
new_esEs27(xx3000, xx4000, app(app(ty_Either, bhb), bhc)) → new_esEs6(xx3000, xx4000, bhb, bhc)
new_esEs21(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs5(xx300, xx400, app(ty_Ratio, fa)) → new_esEs16(xx300, xx400, fa)
new_esEs24(xx3002, xx4002, ty_Int) → new_esEs15(xx3002, xx4002)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_Maybe, dh)) → new_esEs17(xx3000, xx4000, dh)
new_esEs4(xx300, xx400, ty_Float) → new_esEs11(xx300, xx400)
new_esEs27(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs4(xx300, xx400, app(app(ty_@2, ga), gb)) → new_esEs13(xx300, xx400, ga, gb)
new_esEs23(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(app(ty_Either, bah), bba)) → new_esEs6(xx3000, xx4000, bah, bba)
new_esEs27(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs12(Integer(xx3000), Integer(xx4000)) → new_primEqInt(xx3000, xx4000)
new_esEs10(True, True) → True
new_esEs26(xx3000, xx4000, app(app(ty_@2, bfc), bfd)) → new_esEs13(xx3000, xx4000, bfc, bfd)
new_esEs4(xx300, xx400, app(ty_Maybe, ge)) → new_esEs17(xx300, xx400, ge)
new_esEs4(xx300, xx400, app(app(app(ty_@3, gf), gg), gh)) → new_esEs18(xx300, xx400, gf, gg, gh)
new_esEs6(Left(xx3000), Left(xx4000), ty_Integer, bg) → new_esEs12(xx3000, xx4000)
new_primEqNat0(Succ(xx30000), Zero) → False
new_primEqNat0(Zero, Succ(xx40000)) → False
new_esEs6(Left(xx3000), Left(xx4000), ty_Float, bg) → new_esEs11(xx3000, xx4000)
new_primPlusNat0(Zero, Zero) → Zero
new_esEs20(xx3001, xx4001, ty_@0) → new_esEs7(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_Double) → new_esEs9(xx3001, xx4001)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs25(xx3001, xx4001, ty_@0) → new_esEs7(xx3001, xx4001)
new_esEs26(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs14([], [], gc) → True
new_esEs27(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_Ratio, bbh)) → new_esEs16(xx3000, xx4000, bbh)
new_esEs6(Left(xx3000), Left(xx4000), ty_Char, bg) → new_esEs19(xx3000, xx4000)
new_esEs20(xx3001, xx4001, app(app(ty_Either, hf), hg)) → new_esEs6(xx3001, xx4001, hf, hg)
new_esEs15(xx300, xx400) → new_primEqInt(xx300, xx400)
new_primPlusNat1(Succ(xx370), xx400100) → Succ(Succ(new_primPlusNat0(xx370, xx400100)))
new_esEs22(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_[], df)) → new_esEs14(xx3000, xx4000, df)
new_esEs6(Left(xx3000), Left(xx4000), ty_Ordering, bg) → new_esEs8(xx3000, xx4000)
new_esEs4(xx300, xx400, ty_Char) → new_esEs19(xx300, xx400)
new_esEs26(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(ty_@2, dd), de)) → new_esEs13(xx3000, xx4000, dd, de)
new_esEs6(Left(xx3000), Left(xx4000), ty_Double, bg) → new_esEs9(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs19(Char(xx3000), Char(xx4000)) → new_primEqNat0(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(app(ty_@2, bge), bgf)) → new_esEs13(xx3000, xx4000, bge, bgf)
new_esEs8(LT, LT) → True
new_esEs6(Left(xx3000), Right(xx4000), dc, bg) → False
new_esEs6(Right(xx3000), Left(xx4000), dc, bg) → False
new_esEs21(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs18(xx3000, xx4000, bbb, bbc, bbd)
new_esEs25(xx3001, xx4001, ty_Ordering) → new_esEs8(xx3001, xx4001)
new_sr(Neg(xx30010), Neg(xx40010)) → Pos(new_primMulNat0(xx30010, xx40010))
new_esEs21(xx3000, xx4000, app(app(ty_@2, bac), bad)) → new_esEs13(xx3000, xx4000, bac, bad)
new_esEs17(Just(xx3000), Just(xx4000), ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(app(app(ty_@3, cg), da), db), bg) → new_esEs18(xx3000, xx4000, cg, da, db)
new_asAs(False, xx36) → False
new_sr(Pos(xx30010), Pos(xx40010)) → Pos(new_primMulNat0(xx30010, xx40010))
new_esEs11(Float(xx3000, xx3001), Float(xx4000, xx4001)) → new_esEs15(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_primEqNat0(Zero, Zero) → True
new_esEs26(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_primMulNat0(Succ(xx300100), Zero) → Zero
new_primMulNat0(Zero, Succ(xx400100)) → Zero
new_esEs14(:(xx3000, xx3001), :(xx4000, xx4001), gc) → new_asAs(new_esEs27(xx3000, xx4000, gc), new_esEs14(xx3001, xx4001, gc))
new_esEs5(xx300, xx400, ty_Char) → new_esEs19(xx300, xx400)
new_esEs4(xx300, xx400, ty_Bool) → new_esEs10(xx300, xx400)
new_primMulNat0(Succ(xx300100), Succ(xx400100)) → new_primPlusNat1(new_primMulNat0(xx300100, Succ(xx400100)), xx400100)
new_esEs17(Just(xx3000), Just(xx4000), app(app(ty_@2, bbe), bbf)) → new_esEs13(xx3000, xx4000, bbe, bbf)
new_esEs21(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_Ratio, dg)) → new_esEs16(xx3000, xx4000, dg)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(ty_Either, ea), eb)) → new_esEs6(xx3000, xx4000, ea, eb)
new_esEs25(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs17(Just(xx3000), Just(xx4000), app(app(ty_Either, bcb), bcc)) → new_esEs6(xx3000, xx4000, bcb, bcc)
new_esEs24(xx3002, xx4002, ty_Float) → new_esEs11(xx3002, xx4002)
new_esEs4(xx300, xx400, ty_Integer) → new_esEs12(xx300, xx400)
new_esEs26(xx3000, xx4000, app(ty_Maybe, bfg)) → new_esEs17(xx3000, xx4000, bfg)
new_esEs4(xx300, xx400, ty_Double) → new_esEs9(xx300, xx400)
new_esEs4(xx300, xx400, app(ty_[], gc)) → new_esEs14(xx300, xx400, gc)
new_esEs21(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs24(xx3002, xx4002, ty_Char) → new_esEs19(xx3002, xx4002)
new_esEs8(GT, GT) → True
new_esEs4(xx300, xx400, app(app(ty_Either, dc), bg)) → new_esEs6(xx300, xx400, dc, bg)
new_esEs6(Left(xx3000), Left(xx4000), app(app(ty_@2, bh), ca), bg) → new_esEs13(xx3000, xx4000, bh, ca)
new_esEs20(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs26(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs8(GT, LT) → False
new_esEs8(LT, GT) → False
new_esEs21(xx3000, xx4000, app(ty_Ratio, baf)) → new_esEs16(xx3000, xx4000, baf)
new_esEs5(xx300, xx400, ty_Int) → new_esEs15(xx300, xx400)
new_esEs25(xx3001, xx4001, app(app(app(ty_@3, beh), bfa), bfb)) → new_esEs18(xx3001, xx4001, beh, bfa, bfb)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(app(app(ty_@3, bhd), bhe), bhf)) → new_esEs18(xx3000, xx4000, bhd, bhe, bhf)
new_esEs6(Left(xx3000), Left(xx4000), ty_Int, bg) → new_esEs15(xx3000, xx4000)
new_esEs13(@2(xx3000, xx3001), @2(xx4000, xx4001), ga, gb) → new_asAs(new_esEs21(xx3000, xx4000, ga), new_esEs20(xx3001, xx4001, gb))
new_primEqInt(Neg(Succ(xx30000)), Neg(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_esEs20(xx3001, xx4001, ty_Ordering) → new_esEs8(xx3001, xx4001)
new_esEs23(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs27(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs22(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs17(Just(xx3000), Just(xx4000), ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs20(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_[], cb), bg) → new_esEs14(xx3000, xx4000, cb)
new_esEs14(:(xx3000, xx3001), [], gc) → False
new_esEs14([], :(xx4000, xx4001), gc) → False
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(app(ty_@3, ec), ed), ee)) → new_esEs18(xx3000, xx4000, ec, ed, ee)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs24(xx3002, xx4002, ty_Bool) → new_esEs10(xx3002, xx4002)
new_esEs26(xx3000, xx4000, app(ty_[], bfe)) → new_esEs14(xx3000, xx4000, bfe)
new_esEs6(Left(xx3000), Left(xx4000), ty_Bool, bg) → new_esEs10(xx3000, xx4000)
new_primEqInt(Neg(Succ(xx30000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(xx40000))) → False
new_esEs8(EQ, EQ) → True
new_esEs17(Nothing, Nothing, ge) → True
new_esEs21(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_primPlusNat1(Zero, xx400100) → Succ(xx400100)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_Maybe, cd), bg) → new_esEs17(xx3000, xx4000, cd)
new_primPlusNat0(Succ(xx3700), Succ(xx4001000)) → Succ(Succ(new_primPlusNat0(xx3700, xx4001000)))
new_esEs26(xx3000, xx4000, app(app(ty_Either, bfh), bga)) → new_esEs6(xx3000, xx4000, bfh, bga)
new_esEs17(Just(xx3000), Just(xx4000), ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs10(False, False) → True
new_esEs27(xx3000, xx4000, app(ty_[], bgg)) → new_esEs14(xx3000, xx4000, bgg)
new_esEs5(xx300, xx400, app(app(app(ty_@3, ff), fg), fh)) → new_esEs18(xx300, xx400, ff, fg, fh)
new_esEs4(xx300, xx400, ty_Int) → new_esEs15(xx300, xx400)
new_asAs(True, xx36) → xx36
new_esEs20(xx3001, xx4001, ty_Double) → new_esEs9(xx3001, xx4001)
new_esEs4(xx300, xx400, ty_@0) → new_esEs7(xx300, xx400)
new_esEs10(False, True) → False
new_esEs10(True, False) → False
new_esEs25(xx3001, xx4001, ty_Float) → new_esEs11(xx3001, xx4001)
new_esEs24(xx3002, xx4002, ty_@0) → new_esEs7(xx3002, xx4002)
new_esEs17(Just(xx3000), Just(xx4000), ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs9(Double(xx3000, xx3001), Double(xx4000, xx4001)) → new_esEs15(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_primEqInt(Pos(Succ(xx30000)), Pos(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_esEs5(xx300, xx400, ty_Bool) → new_esEs10(xx300, xx400)
new_esEs24(xx3002, xx4002, app(ty_Ratio, bdb)) → new_esEs16(xx3002, xx4002, bdb)
new_esEs5(xx300, xx400, app(ty_Maybe, fb)) → new_esEs17(xx300, xx400, fb)
new_esEs17(Just(xx3000), Nothing, ge) → False
new_esEs17(Nothing, Just(xx4000), ge) → False
new_esEs20(xx3001, xx4001, app(ty_[], hc)) → new_esEs14(xx3001, xx4001, hc)
new_esEs21(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs5(xx300, xx400, ty_Ordering) → new_esEs8(xx300, xx400)
new_primEqNat0(Succ(xx30000), Succ(xx40000)) → new_primEqNat0(xx30000, xx40000)
new_esEs27(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(ty_[], bae)) → new_esEs14(xx3000, xx4000, bae)
new_esEs25(xx3001, xx4001, app(app(ty_@2, bea), beb)) → new_esEs13(xx3001, xx4001, bea, beb)
new_esEs21(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs7(@0, @0) → True
new_esEs20(xx3001, xx4001, app(app(ty_@2, ha), hb)) → new_esEs13(xx3001, xx4001, ha, hb)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_Maybe, bca)) → new_esEs17(xx3000, xx4000, bca)
new_esEs24(xx3002, xx4002, ty_Ordering) → new_esEs8(xx3002, xx4002)
new_esEs4(xx300, xx400, app(ty_Ratio, gd)) → new_esEs16(xx300, xx400, gd)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs18(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), gf, gg, gh) → new_asAs(new_esEs26(xx3000, xx4000, gf), new_asAs(new_esEs25(xx3001, xx4001, gg), new_esEs24(xx3002, xx4002, gh)))
new_esEs8(EQ, LT) → False
new_esEs8(LT, EQ) → False
new_primEqInt(Pos(Zero), Pos(Succ(xx40000))) → False
new_primEqInt(Pos(Succ(xx30000)), Pos(Zero)) → False
new_esEs21(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs5(xx300, xx400, app(app(ty_@2, ef), eg)) → new_esEs13(xx300, xx400, ef, eg)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primPlusNat0(Succ(xx3700), Zero) → Succ(xx3700)
new_primPlusNat0(Zero, Succ(xx4001000)) → Succ(xx4001000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_[], bbg)) → new_esEs14(xx3000, xx4000, bbg)
new_esEs20(xx3001, xx4001, app(app(app(ty_@3, hh), baa), bab)) → new_esEs18(xx3001, xx4001, hh, baa, bab)

The set Q consists of the following terms:

new_esEs6(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs27(x0, x1, ty_@0)
new_esEs17(Nothing, Nothing, x0)
new_esEs6(Right(x0), Right(x1), x2, ty_Char)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs7(@0, @0)
new_primMulNat0(Succ(x0), Zero)
new_esEs21(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Char)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs27(x0, x1, ty_Bool)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs4(x0, x1, ty_Double)
new_esEs18(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Char)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Bool)
new_esEs6(Right(x0), Right(x1), x2, ty_Int)
new_primEqNat0(Succ(x0), Zero)
new_esEs22(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs14(:(x0, x1), [], x2)
new_esEs8(EQ, EQ)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Double)
new_esEs15(x0, x1)
new_esEs6(Right(x0), Right(x1), x2, ty_Double)
new_esEs21(x0, x1, ty_Ordering)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(x0, x1, ty_Int)
new_esEs17(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs5(x0, x1, ty_Float)
new_esEs11(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, ty_Float)
new_asAs(True, x0)
new_primMulNat0(Zero, Succ(x0))
new_esEs6(Left(x0), Left(x1), ty_Float, x2)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(Integer(x0), Integer(x1))
new_esEs24(x0, x1, ty_Double)
new_esEs8(GT, GT)
new_esEs25(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), ty_Integer, x2)
new_esEs6(Left(x0), Left(x1), ty_Int, x2)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs17(Just(x0), Just(x1), ty_Float)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, ty_@0)
new_esEs6(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs6(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs27(x0, x1, ty_Int)
new_esEs17(Just(x0), Just(x1), app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs8(LT, LT)
new_esEs27(x0, x1, ty_Char)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs17(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs14(:(x0, x1), :(x2, x3), x4)
new_esEs17(Just(x0), Just(x1), ty_Int)
new_esEs6(Left(x0), Left(x1), ty_@0, x2)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_sr(Neg(x0), Neg(x1))
new_esEs9(Double(x0, x1), Double(x2, x3))
new_primPlusNat0(Succ(x0), Zero)
new_esEs8(GT, EQ)
new_esEs8(EQ, GT)
new_esEs21(x0, x1, ty_Char)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs19(Char(x0), Char(x1))
new_esEs6(Right(x0), Right(x1), x2, ty_Integer)
new_esEs26(x0, x1, ty_Float)
new_esEs20(x0, x1, app(ty_[], x2))
new_sr(Pos(x0), Pos(x1))
new_esEs5(x0, x1, ty_Bool)
new_esEs6(Left(x0), Left(x1), ty_Char, x2)
new_esEs20(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Bool)
new_esEs8(LT, GT)
new_esEs8(GT, LT)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs27(x0, x1, ty_Double)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Integer)
new_esEs17(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs10(False, False)
new_esEs20(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Float)
new_esEs20(x0, x1, ty_Int)
new_primEqNat0(Zero, Zero)
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs25(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_@0)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Ordering)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_@0)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs26(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs17(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Right(x0), Right(x1), x2, ty_@0)
new_esEs6(Left(x0), Left(x1), ty_Double, x2)
new_esEs26(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_primMulNat0(Zero, Zero)
new_esEs26(x0, x1, ty_Ordering)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Ordering)
new_esEs6(Right(x0), Left(x1), x2, x3)
new_esEs6(Left(x0), Right(x1), x2, x3)
new_esEs17(Just(x0), Just(x1), ty_Char)
new_esEs23(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Char)
new_asAs(False, x0)
new_primPlusNat1(Succ(x0), x1)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Int)
new_esEs17(Just(x0), Nothing, x1)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs13(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs4(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Float)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs20(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs6(Left(x0), Left(x1), ty_Bool, x2)
new_esEs17(Just(x0), Just(x1), ty_@0)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs25(x0, x1, ty_Double)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs17(Just(x0), Just(x1), ty_Bool)
new_esEs17(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_@0)
new_esEs8(EQ, LT)
new_esEs8(LT, EQ)
new_esEs6(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs4(x0, x1, ty_Int)
new_esEs6(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs24(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Int)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs14([], :(x0, x1), x2)
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Zero, Succ(x0))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_Bool)
new_primPlusNat0(Zero, Zero)
new_esEs10(True, True)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Double)
new_esEs14([], [], x0)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs26(x0, x1, ty_Char)
new_esEs16(:%(x0, x1), :%(x2, x3), x4)
new_esEs21(x0, x1, ty_Bool)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Double)
new_esEs17(Nothing, Just(x0), x1)
new_esEs5(x0, x1, ty_Ordering)
new_esEs17(Just(x0), Just(x1), ty_Ordering)
new_esEs20(x0, x1, ty_Float)
new_primPlusNat0(Zero, Succ(x0))
new_esEs4(x0, x1, ty_Float)
new_esEs6(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Float)
new_esEs5(x0, x1, ty_Char)
new_esEs24(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Float)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs17(Just(x0), Just(x1), ty_Double)
new_primPlusNat1(Zero, x0)
new_esEs4(x0, x1, ty_Integer)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Int)
new_esEs5(x0, x1, ty_@0)
new_esEs17(Just(x0), Just(x1), ty_Integer)
new_esEs25(x0, x1, ty_@0)
new_esEs4(x0, x1, app(ty_[], x2))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                  ↳ UsableRulesProof
                                ↳ QDP
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs1(xx20, False, xx22, xx23, be, bf) → new_psPs0(Right(xx20), xx22, xx23, be, bf)
new_psPs0(Right(xx300), :(Left(xx400), xx41), xx5, bc, bd) → new_psPs1(xx300, False, xx41, xx5, bc, bd)
new_psPs0(Right(xx300), :(Right(xx400), xx41), xx5, bc, bd) → new_psPs1(xx300, new_esEs5(xx300, xx400, bd), xx41, xx5, bc, bd)

The TRS R consists of the following rules:

new_esEs25(xx3001, xx4001, app(ty_[], bec)) → new_esEs14(xx3001, xx4001, bec)
new_esEs25(xx3001, xx4001, ty_Char) → new_esEs19(xx3001, xx4001)
new_esEs27(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs20(xx3001, xx4001, app(ty_Maybe, he)) → new_esEs17(xx3001, xx4001, he)
new_esEs27(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs25(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Bool) → new_esEs10(xx3000, xx4000)
new_primEqInt(Neg(Succ(xx30000)), Pos(xx4000)) → False
new_primEqInt(Pos(Succ(xx30000)), Neg(xx4000)) → False
new_esEs5(xx300, xx400, ty_Integer) → new_esEs12(xx300, xx400)
new_esEs16(:%(xx3000, xx3001), :%(xx4000, xx4001), gd) → new_asAs(new_esEs23(xx3000, xx4000, gd), new_esEs22(xx3001, xx4001, gd))
new_esEs26(xx3000, xx4000, app(ty_Ratio, bff)) → new_esEs16(xx3000, xx4000, bff)
new_primEqInt(Pos(Zero), Neg(Succ(xx40000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(xx40000))) → False
new_esEs6(Left(xx3000), Left(xx4000), ty_@0, bg) → new_esEs7(xx3000, xx4000)
new_esEs5(xx300, xx400, app(ty_[], eh)) → new_esEs14(xx300, xx400, eh)
new_esEs25(xx3001, xx4001, app(ty_Maybe, bee)) → new_esEs17(xx3001, xx4001, bee)
new_esEs24(xx3002, xx4002, app(ty_Maybe, bdc)) → new_esEs17(xx3002, xx4002, bdc)
new_esEs5(xx300, xx400, ty_@0) → new_esEs7(xx300, xx400)
new_esEs20(xx3001, xx4001, ty_Bool) → new_esEs10(xx3001, xx4001)
new_esEs8(GT, EQ) → False
new_esEs8(EQ, GT) → False
new_esEs20(xx3001, xx4001, ty_Char) → new_esEs19(xx3001, xx4001)
new_esEs24(xx3002, xx4002, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs18(xx3002, xx4002, bdf, bdg, bdh)
new_esEs17(Just(xx3000), Just(xx4000), app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs18(xx3000, xx4000, bcd, bce, bcf)
new_primMulNat0(Zero, Zero) → Zero
new_esEs27(xx3000, xx4000, app(ty_Ratio, bgh)) → new_esEs16(xx3000, xx4000, bgh)
new_esEs25(xx3001, xx4001, ty_Bool) → new_esEs10(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(app(ty_Either, bef), beg)) → new_esEs6(xx3001, xx4001, bef, beg)
new_esEs5(xx300, xx400, ty_Double) → new_esEs9(xx300, xx400)
new_esEs6(Left(xx3000), Left(xx4000), app(app(ty_Either, ce), cf), bg) → new_esEs6(xx3000, xx4000, ce, cf)
new_esEs4(xx300, xx400, ty_Ordering) → new_esEs8(xx300, xx400)
new_esEs5(xx300, xx400, app(app(ty_Either, fc), fd)) → new_esEs6(xx300, xx400, fc, fd)
new_esEs20(xx3001, xx4001, app(ty_Ratio, hd)) → new_esEs16(xx3001, xx4001, hd)
new_esEs24(xx3002, xx4002, ty_Double) → new_esEs9(xx3002, xx4002)
new_esEs17(Just(xx3000), Just(xx4000), ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_Ratio, cc), bg) → new_esEs16(xx3000, xx4000, cc)
new_esEs27(xx3000, xx4000, app(ty_Maybe, bha)) → new_esEs17(xx3000, xx4000, bha)
new_esEs26(xx3000, xx4000, app(app(app(ty_@3, bgb), bgc), bgd)) → new_esEs18(xx3000, xx4000, bgb, bgc, bgd)
new_esEs24(xx3002, xx4002, app(app(ty_Either, bdd), bde)) → new_esEs6(xx3002, xx4002, bdd, bde)
new_esEs27(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs24(xx3002, xx4002, app(app(ty_@2, bcg), bch)) → new_esEs13(xx3002, xx4002, bcg, bch)
new_esEs17(Just(xx3000), Just(xx4000), ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(ty_Maybe, bag)) → new_esEs17(xx3000, xx4000, bag)
new_esEs25(xx3001, xx4001, app(ty_Ratio, bed)) → new_esEs16(xx3001, xx4001, bed)
new_esEs24(xx3002, xx4002, app(ty_[], bda)) → new_esEs14(xx3002, xx4002, bda)
new_esEs26(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs5(xx300, xx400, ty_Float) → new_esEs11(xx300, xx400)
new_esEs24(xx3002, xx4002, ty_Integer) → new_esEs12(xx3002, xx4002)
new_sr(Pos(xx30010), Neg(xx40010)) → Neg(new_primMulNat0(xx30010, xx40010))
new_sr(Neg(xx30010), Pos(xx40010)) → Neg(new_primMulNat0(xx30010, xx40010))
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs20(xx3001, xx4001, ty_Float) → new_esEs11(xx3001, xx4001)
new_esEs27(xx3000, xx4000, app(app(ty_Either, bhb), bhc)) → new_esEs6(xx3000, xx4000, bhb, bhc)
new_esEs21(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs5(xx300, xx400, app(ty_Ratio, fa)) → new_esEs16(xx300, xx400, fa)
new_esEs24(xx3002, xx4002, ty_Int) → new_esEs15(xx3002, xx4002)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_Maybe, dh)) → new_esEs17(xx3000, xx4000, dh)
new_esEs4(xx300, xx400, ty_Float) → new_esEs11(xx300, xx400)
new_esEs27(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs4(xx300, xx400, app(app(ty_@2, ga), gb)) → new_esEs13(xx300, xx400, ga, gb)
new_esEs23(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(app(ty_Either, bah), bba)) → new_esEs6(xx3000, xx4000, bah, bba)
new_esEs27(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs12(Integer(xx3000), Integer(xx4000)) → new_primEqInt(xx3000, xx4000)
new_esEs10(True, True) → True
new_esEs26(xx3000, xx4000, app(app(ty_@2, bfc), bfd)) → new_esEs13(xx3000, xx4000, bfc, bfd)
new_esEs4(xx300, xx400, app(ty_Maybe, ge)) → new_esEs17(xx300, xx400, ge)
new_esEs4(xx300, xx400, app(app(app(ty_@3, gf), gg), gh)) → new_esEs18(xx300, xx400, gf, gg, gh)
new_esEs6(Left(xx3000), Left(xx4000), ty_Integer, bg) → new_esEs12(xx3000, xx4000)
new_primEqNat0(Succ(xx30000), Zero) → False
new_primEqNat0(Zero, Succ(xx40000)) → False
new_esEs6(Left(xx3000), Left(xx4000), ty_Float, bg) → new_esEs11(xx3000, xx4000)
new_primPlusNat0(Zero, Zero) → Zero
new_esEs20(xx3001, xx4001, ty_@0) → new_esEs7(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_Double) → new_esEs9(xx3001, xx4001)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs25(xx3001, xx4001, ty_@0) → new_esEs7(xx3001, xx4001)
new_esEs26(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs14([], [], gc) → True
new_esEs27(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_Ratio, bbh)) → new_esEs16(xx3000, xx4000, bbh)
new_esEs6(Left(xx3000), Left(xx4000), ty_Char, bg) → new_esEs19(xx3000, xx4000)
new_esEs20(xx3001, xx4001, app(app(ty_Either, hf), hg)) → new_esEs6(xx3001, xx4001, hf, hg)
new_esEs15(xx300, xx400) → new_primEqInt(xx300, xx400)
new_primPlusNat1(Succ(xx370), xx400100) → Succ(Succ(new_primPlusNat0(xx370, xx400100)))
new_esEs22(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_[], df)) → new_esEs14(xx3000, xx4000, df)
new_esEs6(Left(xx3000), Left(xx4000), ty_Ordering, bg) → new_esEs8(xx3000, xx4000)
new_esEs4(xx300, xx400, ty_Char) → new_esEs19(xx300, xx400)
new_esEs26(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(ty_@2, dd), de)) → new_esEs13(xx3000, xx4000, dd, de)
new_esEs6(Left(xx3000), Left(xx4000), ty_Double, bg) → new_esEs9(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs19(Char(xx3000), Char(xx4000)) → new_primEqNat0(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(app(ty_@2, bge), bgf)) → new_esEs13(xx3000, xx4000, bge, bgf)
new_esEs8(LT, LT) → True
new_esEs6(Left(xx3000), Right(xx4000), dc, bg) → False
new_esEs6(Right(xx3000), Left(xx4000), dc, bg) → False
new_esEs21(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs18(xx3000, xx4000, bbb, bbc, bbd)
new_esEs25(xx3001, xx4001, ty_Ordering) → new_esEs8(xx3001, xx4001)
new_sr(Neg(xx30010), Neg(xx40010)) → Pos(new_primMulNat0(xx30010, xx40010))
new_esEs21(xx3000, xx4000, app(app(ty_@2, bac), bad)) → new_esEs13(xx3000, xx4000, bac, bad)
new_esEs17(Just(xx3000), Just(xx4000), ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(app(app(ty_@3, cg), da), db), bg) → new_esEs18(xx3000, xx4000, cg, da, db)
new_asAs(False, xx36) → False
new_sr(Pos(xx30010), Pos(xx40010)) → Pos(new_primMulNat0(xx30010, xx40010))
new_esEs11(Float(xx3000, xx3001), Float(xx4000, xx4001)) → new_esEs15(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_primEqNat0(Zero, Zero) → True
new_esEs26(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_primMulNat0(Succ(xx300100), Zero) → Zero
new_primMulNat0(Zero, Succ(xx400100)) → Zero
new_esEs14(:(xx3000, xx3001), :(xx4000, xx4001), gc) → new_asAs(new_esEs27(xx3000, xx4000, gc), new_esEs14(xx3001, xx4001, gc))
new_esEs5(xx300, xx400, ty_Char) → new_esEs19(xx300, xx400)
new_esEs4(xx300, xx400, ty_Bool) → new_esEs10(xx300, xx400)
new_primMulNat0(Succ(xx300100), Succ(xx400100)) → new_primPlusNat1(new_primMulNat0(xx300100, Succ(xx400100)), xx400100)
new_esEs17(Just(xx3000), Just(xx4000), app(app(ty_@2, bbe), bbf)) → new_esEs13(xx3000, xx4000, bbe, bbf)
new_esEs21(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_Ratio, dg)) → new_esEs16(xx3000, xx4000, dg)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(ty_Either, ea), eb)) → new_esEs6(xx3000, xx4000, ea, eb)
new_esEs25(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs17(Just(xx3000), Just(xx4000), app(app(ty_Either, bcb), bcc)) → new_esEs6(xx3000, xx4000, bcb, bcc)
new_esEs24(xx3002, xx4002, ty_Float) → new_esEs11(xx3002, xx4002)
new_esEs4(xx300, xx400, ty_Integer) → new_esEs12(xx300, xx400)
new_esEs26(xx3000, xx4000, app(ty_Maybe, bfg)) → new_esEs17(xx3000, xx4000, bfg)
new_esEs4(xx300, xx400, ty_Double) → new_esEs9(xx300, xx400)
new_esEs4(xx300, xx400, app(ty_[], gc)) → new_esEs14(xx300, xx400, gc)
new_esEs21(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs24(xx3002, xx4002, ty_Char) → new_esEs19(xx3002, xx4002)
new_esEs8(GT, GT) → True
new_esEs4(xx300, xx400, app(app(ty_Either, dc), bg)) → new_esEs6(xx300, xx400, dc, bg)
new_esEs6(Left(xx3000), Left(xx4000), app(app(ty_@2, bh), ca), bg) → new_esEs13(xx3000, xx4000, bh, ca)
new_esEs20(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs26(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs8(GT, LT) → False
new_esEs8(LT, GT) → False
new_esEs21(xx3000, xx4000, app(ty_Ratio, baf)) → new_esEs16(xx3000, xx4000, baf)
new_esEs5(xx300, xx400, ty_Int) → new_esEs15(xx300, xx400)
new_esEs25(xx3001, xx4001, app(app(app(ty_@3, beh), bfa), bfb)) → new_esEs18(xx3001, xx4001, beh, bfa, bfb)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(app(app(ty_@3, bhd), bhe), bhf)) → new_esEs18(xx3000, xx4000, bhd, bhe, bhf)
new_esEs6(Left(xx3000), Left(xx4000), ty_Int, bg) → new_esEs15(xx3000, xx4000)
new_esEs13(@2(xx3000, xx3001), @2(xx4000, xx4001), ga, gb) → new_asAs(new_esEs21(xx3000, xx4000, ga), new_esEs20(xx3001, xx4001, gb))
new_primEqInt(Neg(Succ(xx30000)), Neg(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_esEs20(xx3001, xx4001, ty_Ordering) → new_esEs8(xx3001, xx4001)
new_esEs23(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs27(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs22(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs17(Just(xx3000), Just(xx4000), ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs20(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_[], cb), bg) → new_esEs14(xx3000, xx4000, cb)
new_esEs14(:(xx3000, xx3001), [], gc) → False
new_esEs14([], :(xx4000, xx4001), gc) → False
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(app(ty_@3, ec), ed), ee)) → new_esEs18(xx3000, xx4000, ec, ed, ee)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs24(xx3002, xx4002, ty_Bool) → new_esEs10(xx3002, xx4002)
new_esEs26(xx3000, xx4000, app(ty_[], bfe)) → new_esEs14(xx3000, xx4000, bfe)
new_esEs6(Left(xx3000), Left(xx4000), ty_Bool, bg) → new_esEs10(xx3000, xx4000)
new_primEqInt(Neg(Succ(xx30000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(xx40000))) → False
new_esEs8(EQ, EQ) → True
new_esEs17(Nothing, Nothing, ge) → True
new_esEs21(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_primPlusNat1(Zero, xx400100) → Succ(xx400100)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_Maybe, cd), bg) → new_esEs17(xx3000, xx4000, cd)
new_primPlusNat0(Succ(xx3700), Succ(xx4001000)) → Succ(Succ(new_primPlusNat0(xx3700, xx4001000)))
new_esEs26(xx3000, xx4000, app(app(ty_Either, bfh), bga)) → new_esEs6(xx3000, xx4000, bfh, bga)
new_esEs17(Just(xx3000), Just(xx4000), ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs10(False, False) → True
new_esEs27(xx3000, xx4000, app(ty_[], bgg)) → new_esEs14(xx3000, xx4000, bgg)
new_esEs5(xx300, xx400, app(app(app(ty_@3, ff), fg), fh)) → new_esEs18(xx300, xx400, ff, fg, fh)
new_esEs4(xx300, xx400, ty_Int) → new_esEs15(xx300, xx400)
new_asAs(True, xx36) → xx36
new_esEs20(xx3001, xx4001, ty_Double) → new_esEs9(xx3001, xx4001)
new_esEs4(xx300, xx400, ty_@0) → new_esEs7(xx300, xx400)
new_esEs10(False, True) → False
new_esEs10(True, False) → False
new_esEs25(xx3001, xx4001, ty_Float) → new_esEs11(xx3001, xx4001)
new_esEs24(xx3002, xx4002, ty_@0) → new_esEs7(xx3002, xx4002)
new_esEs17(Just(xx3000), Just(xx4000), ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs9(Double(xx3000, xx3001), Double(xx4000, xx4001)) → new_esEs15(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_primEqInt(Pos(Succ(xx30000)), Pos(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_esEs5(xx300, xx400, ty_Bool) → new_esEs10(xx300, xx400)
new_esEs24(xx3002, xx4002, app(ty_Ratio, bdb)) → new_esEs16(xx3002, xx4002, bdb)
new_esEs5(xx300, xx400, app(ty_Maybe, fb)) → new_esEs17(xx300, xx400, fb)
new_esEs17(Just(xx3000), Nothing, ge) → False
new_esEs17(Nothing, Just(xx4000), ge) → False
new_esEs20(xx3001, xx4001, app(ty_[], hc)) → new_esEs14(xx3001, xx4001, hc)
new_esEs21(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs5(xx300, xx400, ty_Ordering) → new_esEs8(xx300, xx400)
new_primEqNat0(Succ(xx30000), Succ(xx40000)) → new_primEqNat0(xx30000, xx40000)
new_esEs27(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(ty_[], bae)) → new_esEs14(xx3000, xx4000, bae)
new_esEs25(xx3001, xx4001, app(app(ty_@2, bea), beb)) → new_esEs13(xx3001, xx4001, bea, beb)
new_esEs21(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs7(@0, @0) → True
new_esEs20(xx3001, xx4001, app(app(ty_@2, ha), hb)) → new_esEs13(xx3001, xx4001, ha, hb)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_Maybe, bca)) → new_esEs17(xx3000, xx4000, bca)
new_esEs24(xx3002, xx4002, ty_Ordering) → new_esEs8(xx3002, xx4002)
new_esEs4(xx300, xx400, app(ty_Ratio, gd)) → new_esEs16(xx300, xx400, gd)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs18(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), gf, gg, gh) → new_asAs(new_esEs26(xx3000, xx4000, gf), new_asAs(new_esEs25(xx3001, xx4001, gg), new_esEs24(xx3002, xx4002, gh)))
new_esEs8(EQ, LT) → False
new_esEs8(LT, EQ) → False
new_primEqInt(Pos(Zero), Pos(Succ(xx40000))) → False
new_primEqInt(Pos(Succ(xx30000)), Pos(Zero)) → False
new_esEs21(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs5(xx300, xx400, app(app(ty_@2, ef), eg)) → new_esEs13(xx300, xx400, ef, eg)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primPlusNat0(Succ(xx3700), Zero) → Succ(xx3700)
new_primPlusNat0(Zero, Succ(xx4001000)) → Succ(xx4001000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_[], bbg)) → new_esEs14(xx3000, xx4000, bbg)
new_esEs20(xx3001, xx4001, app(app(app(ty_@3, hh), baa), bab)) → new_esEs18(xx3001, xx4001, hh, baa, bab)

The set Q consists of the following terms:

new_esEs6(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs27(x0, x1, ty_@0)
new_esEs17(Nothing, Nothing, x0)
new_esEs6(Right(x0), Right(x1), x2, ty_Char)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs7(@0, @0)
new_primMulNat0(Succ(x0), Zero)
new_esEs21(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Char)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs27(x0, x1, ty_Bool)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs4(x0, x1, ty_Double)
new_esEs18(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Char)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Bool)
new_esEs6(Right(x0), Right(x1), x2, ty_Int)
new_primEqNat0(Succ(x0), Zero)
new_esEs22(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs14(:(x0, x1), [], x2)
new_esEs8(EQ, EQ)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Double)
new_esEs15(x0, x1)
new_esEs6(Right(x0), Right(x1), x2, ty_Double)
new_esEs21(x0, x1, ty_Ordering)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(x0, x1, ty_Int)
new_esEs17(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs5(x0, x1, ty_Float)
new_esEs11(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, ty_Float)
new_asAs(True, x0)
new_primMulNat0(Zero, Succ(x0))
new_esEs6(Left(x0), Left(x1), ty_Float, x2)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(Integer(x0), Integer(x1))
new_esEs24(x0, x1, ty_Double)
new_esEs8(GT, GT)
new_esEs25(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), ty_Integer, x2)
new_esEs6(Left(x0), Left(x1), ty_Int, x2)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs17(Just(x0), Just(x1), ty_Float)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, ty_@0)
new_esEs6(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs6(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs27(x0, x1, ty_Int)
new_esEs17(Just(x0), Just(x1), app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs8(LT, LT)
new_esEs27(x0, x1, ty_Char)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs17(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs14(:(x0, x1), :(x2, x3), x4)
new_esEs17(Just(x0), Just(x1), ty_Int)
new_esEs6(Left(x0), Left(x1), ty_@0, x2)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_sr(Neg(x0), Neg(x1))
new_esEs9(Double(x0, x1), Double(x2, x3))
new_primPlusNat0(Succ(x0), Zero)
new_esEs8(GT, EQ)
new_esEs8(EQ, GT)
new_esEs21(x0, x1, ty_Char)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs19(Char(x0), Char(x1))
new_esEs6(Right(x0), Right(x1), x2, ty_Integer)
new_esEs26(x0, x1, ty_Float)
new_esEs20(x0, x1, app(ty_[], x2))
new_sr(Pos(x0), Pos(x1))
new_esEs5(x0, x1, ty_Bool)
new_esEs6(Left(x0), Left(x1), ty_Char, x2)
new_esEs20(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Bool)
new_esEs8(LT, GT)
new_esEs8(GT, LT)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs27(x0, x1, ty_Double)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Integer)
new_esEs17(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs10(False, False)
new_esEs20(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Float)
new_esEs20(x0, x1, ty_Int)
new_primEqNat0(Zero, Zero)
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs25(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_@0)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Ordering)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_@0)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs26(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs17(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Right(x0), Right(x1), x2, ty_@0)
new_esEs6(Left(x0), Left(x1), ty_Double, x2)
new_esEs26(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_primMulNat0(Zero, Zero)
new_esEs26(x0, x1, ty_Ordering)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Ordering)
new_esEs6(Right(x0), Left(x1), x2, x3)
new_esEs6(Left(x0), Right(x1), x2, x3)
new_esEs17(Just(x0), Just(x1), ty_Char)
new_esEs23(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Char)
new_asAs(False, x0)
new_primPlusNat1(Succ(x0), x1)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Int)
new_esEs17(Just(x0), Nothing, x1)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs13(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs4(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Float)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs20(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs6(Left(x0), Left(x1), ty_Bool, x2)
new_esEs17(Just(x0), Just(x1), ty_@0)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs25(x0, x1, ty_Double)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs17(Just(x0), Just(x1), ty_Bool)
new_esEs17(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_@0)
new_esEs8(EQ, LT)
new_esEs8(LT, EQ)
new_esEs6(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs4(x0, x1, ty_Int)
new_esEs6(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs24(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Int)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs14([], :(x0, x1), x2)
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Zero, Succ(x0))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_Bool)
new_primPlusNat0(Zero, Zero)
new_esEs10(True, True)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Double)
new_esEs14([], [], x0)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs26(x0, x1, ty_Char)
new_esEs16(:%(x0, x1), :%(x2, x3), x4)
new_esEs21(x0, x1, ty_Bool)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Double)
new_esEs17(Nothing, Just(x0), x1)
new_esEs5(x0, x1, ty_Ordering)
new_esEs17(Just(x0), Just(x1), ty_Ordering)
new_esEs20(x0, x1, ty_Float)
new_primPlusNat0(Zero, Succ(x0))
new_esEs4(x0, x1, ty_Float)
new_esEs6(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Float)
new_esEs5(x0, x1, ty_Char)
new_esEs24(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Float)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs17(Just(x0), Just(x1), ty_Double)
new_primPlusNat1(Zero, x0)
new_esEs4(x0, x1, ty_Integer)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Int)
new_esEs5(x0, x1, ty_@0)
new_esEs17(Just(x0), Just(x1), ty_Integer)
new_esEs25(x0, x1, ty_@0)
new_esEs4(x0, x1, app(ty_[], x2))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                ↳ QDP
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs1(xx20, False, xx22, xx23, be, bf) → new_psPs0(Right(xx20), xx22, xx23, be, bf)
new_psPs0(Right(xx300), :(Left(xx400), xx41), xx5, bc, bd) → new_psPs1(xx300, False, xx41, xx5, bc, bd)
new_psPs0(Right(xx300), :(Right(xx400), xx41), xx5, bc, bd) → new_psPs1(xx300, new_esEs5(xx300, xx400, bd), xx41, xx5, bc, bd)

The TRS R consists of the following rules:

new_esEs5(xx300, xx400, ty_Integer) → new_esEs12(xx300, xx400)
new_esEs5(xx300, xx400, app(ty_[], eh)) → new_esEs14(xx300, xx400, eh)
new_esEs5(xx300, xx400, ty_@0) → new_esEs7(xx300, xx400)
new_esEs5(xx300, xx400, ty_Double) → new_esEs9(xx300, xx400)
new_esEs5(xx300, xx400, app(app(ty_Either, fc), fd)) → new_esEs6(xx300, xx400, fc, fd)
new_esEs5(xx300, xx400, ty_Float) → new_esEs11(xx300, xx400)
new_esEs5(xx300, xx400, app(ty_Ratio, fa)) → new_esEs16(xx300, xx400, fa)
new_esEs5(xx300, xx400, ty_Char) → new_esEs19(xx300, xx400)
new_esEs5(xx300, xx400, ty_Int) → new_esEs15(xx300, xx400)
new_esEs5(xx300, xx400, app(app(app(ty_@3, ff), fg), fh)) → new_esEs18(xx300, xx400, ff, fg, fh)
new_esEs5(xx300, xx400, ty_Bool) → new_esEs10(xx300, xx400)
new_esEs5(xx300, xx400, app(ty_Maybe, fb)) → new_esEs17(xx300, xx400, fb)
new_esEs5(xx300, xx400, ty_Ordering) → new_esEs8(xx300, xx400)
new_esEs5(xx300, xx400, app(app(ty_@2, ef), eg)) → new_esEs13(xx300, xx400, ef, eg)
new_esEs13(@2(xx3000, xx3001), @2(xx4000, xx4001), ga, gb) → new_asAs(new_esEs21(xx3000, xx4000, ga), new_esEs20(xx3001, xx4001, gb))
new_esEs21(xx3000, xx4000, app(ty_Maybe, bag)) → new_esEs17(xx3000, xx4000, bag)
new_esEs21(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(app(ty_Either, bah), bba)) → new_esEs6(xx3000, xx4000, bah, bba)
new_esEs21(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs18(xx3000, xx4000, bbb, bbc, bbd)
new_esEs21(xx3000, xx4000, app(app(ty_@2, bac), bad)) → new_esEs13(xx3000, xx4000, bac, bad)
new_esEs21(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs21(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(ty_Ratio, baf)) → new_esEs16(xx3000, xx4000, baf)
new_esEs21(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs21(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(ty_[], bae)) → new_esEs14(xx3000, xx4000, bae)
new_esEs21(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs21(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs20(xx3001, xx4001, app(ty_Maybe, he)) → new_esEs17(xx3001, xx4001, he)
new_esEs20(xx3001, xx4001, ty_Bool) → new_esEs10(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_Char) → new_esEs19(xx3001, xx4001)
new_esEs20(xx3001, xx4001, app(ty_Ratio, hd)) → new_esEs16(xx3001, xx4001, hd)
new_esEs20(xx3001, xx4001, ty_Float) → new_esEs11(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_@0) → new_esEs7(xx3001, xx4001)
new_esEs20(xx3001, xx4001, app(app(ty_Either, hf), hg)) → new_esEs6(xx3001, xx4001, hf, hg)
new_esEs20(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_Ordering) → new_esEs8(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_Double) → new_esEs9(xx3001, xx4001)
new_esEs20(xx3001, xx4001, app(ty_[], hc)) → new_esEs14(xx3001, xx4001, hc)
new_esEs20(xx3001, xx4001, app(app(ty_@2, ha), hb)) → new_esEs13(xx3001, xx4001, ha, hb)
new_esEs20(xx3001, xx4001, app(app(app(ty_@3, hh), baa), bab)) → new_esEs18(xx3001, xx4001, hh, baa, bab)
new_asAs(False, xx36) → False
new_asAs(True, xx36) → xx36
new_esEs18(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), gf, gg, gh) → new_asAs(new_esEs26(xx3000, xx4000, gf), new_asAs(new_esEs25(xx3001, xx4001, gg), new_esEs24(xx3002, xx4002, gh)))
new_esEs26(xx3000, xx4000, app(ty_Ratio, bff)) → new_esEs16(xx3000, xx4000, bff)
new_esEs26(xx3000, xx4000, app(app(app(ty_@3, bgb), bgc), bgd)) → new_esEs18(xx3000, xx4000, bgb, bgc, bgd)
new_esEs26(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs26(xx3000, xx4000, app(app(ty_@2, bfc), bfd)) → new_esEs13(xx3000, xx4000, bfc, bfd)
new_esEs26(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs26(xx3000, xx4000, app(ty_Maybe, bfg)) → new_esEs17(xx3000, xx4000, bfg)
new_esEs26(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs26(xx3000, xx4000, app(ty_[], bfe)) → new_esEs14(xx3000, xx4000, bfe)
new_esEs26(xx3000, xx4000, app(app(ty_Either, bfh), bga)) → new_esEs6(xx3000, xx4000, bfh, bga)
new_esEs26(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs25(xx3001, xx4001, app(ty_[], bec)) → new_esEs14(xx3001, xx4001, bec)
new_esEs25(xx3001, xx4001, ty_Char) → new_esEs19(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(ty_Maybe, bee)) → new_esEs17(xx3001, xx4001, bee)
new_esEs25(xx3001, xx4001, ty_Bool) → new_esEs10(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(app(ty_Either, bef), beg)) → new_esEs6(xx3001, xx4001, bef, beg)
new_esEs25(xx3001, xx4001, app(ty_Ratio, bed)) → new_esEs16(xx3001, xx4001, bed)
new_esEs25(xx3001, xx4001, ty_Double) → new_esEs9(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_@0) → new_esEs7(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_Ordering) → new_esEs8(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(app(app(ty_@3, beh), bfa), bfb)) → new_esEs18(xx3001, xx4001, beh, bfa, bfb)
new_esEs25(xx3001, xx4001, ty_Float) → new_esEs11(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(app(ty_@2, bea), beb)) → new_esEs13(xx3001, xx4001, bea, beb)
new_esEs24(xx3002, xx4002, app(ty_Maybe, bdc)) → new_esEs17(xx3002, xx4002, bdc)
new_esEs24(xx3002, xx4002, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs18(xx3002, xx4002, bdf, bdg, bdh)
new_esEs24(xx3002, xx4002, ty_Double) → new_esEs9(xx3002, xx4002)
new_esEs24(xx3002, xx4002, app(app(ty_Either, bdd), bde)) → new_esEs6(xx3002, xx4002, bdd, bde)
new_esEs24(xx3002, xx4002, app(app(ty_@2, bcg), bch)) → new_esEs13(xx3002, xx4002, bcg, bch)
new_esEs24(xx3002, xx4002, app(ty_[], bda)) → new_esEs14(xx3002, xx4002, bda)
new_esEs24(xx3002, xx4002, ty_Integer) → new_esEs12(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_Int) → new_esEs15(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_Float) → new_esEs11(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_Char) → new_esEs19(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_Bool) → new_esEs10(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_@0) → new_esEs7(xx3002, xx4002)
new_esEs24(xx3002, xx4002, app(ty_Ratio, bdb)) → new_esEs16(xx3002, xx4002, bdb)
new_esEs24(xx3002, xx4002, ty_Ordering) → new_esEs8(xx3002, xx4002)
new_esEs8(GT, EQ) → False
new_esEs8(EQ, GT) → False
new_esEs8(LT, LT) → True
new_esEs8(GT, GT) → True
new_esEs8(GT, LT) → False
new_esEs8(LT, GT) → False
new_esEs8(EQ, EQ) → True
new_esEs8(EQ, LT) → False
new_esEs8(LT, EQ) → False
new_esEs16(:%(xx3000, xx3001), :%(xx4000, xx4001), gd) → new_asAs(new_esEs23(xx3000, xx4000, gd), new_esEs22(xx3001, xx4001, gd))
new_esEs23(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs23(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs22(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs22(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs15(xx300, xx400) → new_primEqInt(xx300, xx400)
new_primEqInt(Neg(Succ(xx30000)), Pos(xx4000)) → False
new_primEqInt(Pos(Succ(xx30000)), Neg(xx4000)) → False
new_primEqInt(Pos(Zero), Neg(Succ(xx40000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(xx40000))) → False
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_primEqInt(Neg(Succ(xx30000)), Neg(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Succ(xx30000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(xx40000))) → False
new_primEqInt(Pos(Succ(xx30000)), Pos(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_primEqInt(Pos(Zero), Pos(Succ(xx40000))) → False
new_primEqInt(Pos(Succ(xx30000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqNat0(Succ(xx30000), Zero) → False
new_primEqNat0(Zero, Succ(xx40000)) → False
new_primEqNat0(Zero, Zero) → True
new_primEqNat0(Succ(xx30000), Succ(xx40000)) → new_primEqNat0(xx30000, xx40000)
new_esEs12(Integer(xx3000), Integer(xx4000)) → new_primEqInt(xx3000, xx4000)
new_esEs7(@0, @0) → True
new_esEs10(True, True) → True
new_esEs10(False, False) → True
new_esEs10(False, True) → False
new_esEs10(True, False) → False
new_esEs19(Char(xx3000), Char(xx4000)) → new_primEqNat0(xx3000, xx4000)
new_esEs11(Float(xx3000, xx3001), Float(xx4000, xx4001)) → new_esEs15(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_sr(Pos(xx30010), Neg(xx40010)) → Neg(new_primMulNat0(xx30010, xx40010))
new_sr(Neg(xx30010), Pos(xx40010)) → Neg(new_primMulNat0(xx30010, xx40010))
new_sr(Neg(xx30010), Neg(xx40010)) → Pos(new_primMulNat0(xx30010, xx40010))
new_sr(Pos(xx30010), Pos(xx40010)) → Pos(new_primMulNat0(xx30010, xx40010))
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Succ(xx300100), Zero) → Zero
new_primMulNat0(Zero, Succ(xx400100)) → Zero
new_primMulNat0(Succ(xx300100), Succ(xx400100)) → new_primPlusNat1(new_primMulNat0(xx300100, Succ(xx400100)), xx400100)
new_primPlusNat1(Succ(xx370), xx400100) → Succ(Succ(new_primPlusNat0(xx370, xx400100)))
new_primPlusNat1(Zero, xx400100) → Succ(xx400100)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(xx3700), Succ(xx4001000)) → Succ(Succ(new_primPlusNat0(xx3700, xx4001000)))
new_primPlusNat0(Succ(xx3700), Zero) → Succ(xx3700)
new_primPlusNat0(Zero, Succ(xx4001000)) → Succ(xx4001000)
new_esEs14([], [], gc) → True
new_esEs14(:(xx3000, xx3001), :(xx4000, xx4001), gc) → new_asAs(new_esEs27(xx3000, xx4000, gc), new_esEs14(xx3001, xx4001, gc))
new_esEs14(:(xx3000, xx3001), [], gc) → False
new_esEs14([], :(xx4000, xx4001), gc) → False
new_esEs27(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs27(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(ty_Ratio, bgh)) → new_esEs16(xx3000, xx4000, bgh)
new_esEs27(xx3000, xx4000, app(ty_Maybe, bha)) → new_esEs17(xx3000, xx4000, bha)
new_esEs27(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(app(ty_Either, bhb), bhc)) → new_esEs6(xx3000, xx4000, bhb, bhc)
new_esEs27(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs27(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs27(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(app(ty_@2, bge), bgf)) → new_esEs13(xx3000, xx4000, bge, bgf)
new_esEs27(xx3000, xx4000, app(app(app(ty_@3, bhd), bhe), bhf)) → new_esEs18(xx3000, xx4000, bhd, bhe, bhf)
new_esEs27(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(ty_[], bgg)) → new_esEs14(xx3000, xx4000, bgg)
new_esEs27(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), ty_@0, bg) → new_esEs7(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_Ratio, cc), bg) → new_esEs16(xx3000, xx4000, cc)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_Maybe, cd), bg) → new_esEs17(xx3000, xx4000, cd)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_Maybe, bca)) → new_esEs17(xx3000, xx4000, bca)
new_esEs17(Just(xx3000), Just(xx4000), app(app(ty_Either, bcb), bcc)) → new_esEs6(xx3000, xx4000, bcb, bcc)
new_esEs6(Left(xx3000), Left(xx4000), app(app(ty_Either, ce), cf), bg) → new_esEs6(xx3000, xx4000, ce, cf)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(ty_Either, ea), eb)) → new_esEs6(xx3000, xx4000, ea, eb)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_Maybe, dh)) → new_esEs17(xx3000, xx4000, dh)
new_esEs6(Left(xx3000), Left(xx4000), ty_Integer, bg) → new_esEs12(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), ty_Float, bg) → new_esEs11(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), ty_Char, bg) → new_esEs19(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_[], df)) → new_esEs14(xx3000, xx4000, df)
new_esEs6(Left(xx3000), Left(xx4000), ty_Ordering, bg) → new_esEs8(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(ty_@2, dd), de)) → new_esEs13(xx3000, xx4000, dd, de)
new_esEs6(Left(xx3000), Left(xx4000), ty_Double, bg) → new_esEs9(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs6(Left(xx3000), Right(xx4000), dc, bg) → False
new_esEs6(Right(xx3000), Left(xx4000), dc, bg) → False
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(app(app(ty_@3, cg), da), db), bg) → new_esEs18(xx3000, xx4000, cg, da, db)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_Ratio, dg)) → new_esEs16(xx3000, xx4000, dg)
new_esEs6(Left(xx3000), Left(xx4000), app(app(ty_@2, bh), ca), bg) → new_esEs13(xx3000, xx4000, bh, ca)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), ty_Int, bg) → new_esEs15(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_[], cb), bg) → new_esEs14(xx3000, xx4000, cb)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(app(ty_@3, ec), ed), ee)) → new_esEs18(xx3000, xx4000, ec, ed, ee)
new_esEs6(Left(xx3000), Left(xx4000), ty_Bool, bg) → new_esEs10(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs9(Double(xx3000, xx3001), Double(xx4000, xx4001)) → new_esEs15(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_esEs17(Just(xx3000), Just(xx4000), app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs18(xx3000, xx4000, bcd, bce, bcf)
new_esEs17(Just(xx3000), Just(xx4000), ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_Ratio, bbh)) → new_esEs16(xx3000, xx4000, bbh)
new_esEs17(Just(xx3000), Just(xx4000), ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), app(app(ty_@2, bbe), bbf)) → new_esEs13(xx3000, xx4000, bbe, bbf)
new_esEs17(Just(xx3000), Just(xx4000), ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs17(Nothing, Nothing, ge) → True
new_esEs17(Just(xx3000), Just(xx4000), ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs17(Just(xx3000), Nothing, ge) → False
new_esEs17(Nothing, Just(xx4000), ge) → False
new_esEs17(Just(xx3000), Just(xx4000), ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_[], bbg)) → new_esEs14(xx3000, xx4000, bbg)

The set Q consists of the following terms:

new_esEs6(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs27(x0, x1, ty_@0)
new_esEs17(Nothing, Nothing, x0)
new_esEs6(Right(x0), Right(x1), x2, ty_Char)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs7(@0, @0)
new_primMulNat0(Succ(x0), Zero)
new_esEs21(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Char)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs27(x0, x1, ty_Bool)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs4(x0, x1, ty_Double)
new_esEs18(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Char)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Bool)
new_esEs6(Right(x0), Right(x1), x2, ty_Int)
new_primEqNat0(Succ(x0), Zero)
new_esEs22(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs14(:(x0, x1), [], x2)
new_esEs8(EQ, EQ)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Double)
new_esEs15(x0, x1)
new_esEs6(Right(x0), Right(x1), x2, ty_Double)
new_esEs21(x0, x1, ty_Ordering)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(x0, x1, ty_Int)
new_esEs17(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs5(x0, x1, ty_Float)
new_esEs11(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, ty_Float)
new_asAs(True, x0)
new_primMulNat0(Zero, Succ(x0))
new_esEs6(Left(x0), Left(x1), ty_Float, x2)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(Integer(x0), Integer(x1))
new_esEs24(x0, x1, ty_Double)
new_esEs8(GT, GT)
new_esEs25(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), ty_Integer, x2)
new_esEs6(Left(x0), Left(x1), ty_Int, x2)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs17(Just(x0), Just(x1), ty_Float)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, ty_@0)
new_esEs6(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs6(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs27(x0, x1, ty_Int)
new_esEs17(Just(x0), Just(x1), app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs8(LT, LT)
new_esEs27(x0, x1, ty_Char)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs17(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs14(:(x0, x1), :(x2, x3), x4)
new_esEs17(Just(x0), Just(x1), ty_Int)
new_esEs6(Left(x0), Left(x1), ty_@0, x2)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_sr(Neg(x0), Neg(x1))
new_esEs9(Double(x0, x1), Double(x2, x3))
new_primPlusNat0(Succ(x0), Zero)
new_esEs8(GT, EQ)
new_esEs8(EQ, GT)
new_esEs21(x0, x1, ty_Char)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs19(Char(x0), Char(x1))
new_esEs6(Right(x0), Right(x1), x2, ty_Integer)
new_esEs26(x0, x1, ty_Float)
new_esEs20(x0, x1, app(ty_[], x2))
new_sr(Pos(x0), Pos(x1))
new_esEs5(x0, x1, ty_Bool)
new_esEs6(Left(x0), Left(x1), ty_Char, x2)
new_esEs20(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Bool)
new_esEs8(LT, GT)
new_esEs8(GT, LT)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs27(x0, x1, ty_Double)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Integer)
new_esEs17(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs10(False, False)
new_esEs20(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Float)
new_esEs20(x0, x1, ty_Int)
new_primEqNat0(Zero, Zero)
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs25(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_@0)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Ordering)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_@0)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs26(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs17(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Right(x0), Right(x1), x2, ty_@0)
new_esEs6(Left(x0), Left(x1), ty_Double, x2)
new_esEs26(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_primMulNat0(Zero, Zero)
new_esEs26(x0, x1, ty_Ordering)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Ordering)
new_esEs6(Right(x0), Left(x1), x2, x3)
new_esEs6(Left(x0), Right(x1), x2, x3)
new_esEs17(Just(x0), Just(x1), ty_Char)
new_esEs23(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Char)
new_asAs(False, x0)
new_primPlusNat1(Succ(x0), x1)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Int)
new_esEs17(Just(x0), Nothing, x1)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs13(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs4(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Float)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs20(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs6(Left(x0), Left(x1), ty_Bool, x2)
new_esEs17(Just(x0), Just(x1), ty_@0)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs25(x0, x1, ty_Double)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs17(Just(x0), Just(x1), ty_Bool)
new_esEs17(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_@0)
new_esEs8(EQ, LT)
new_esEs8(LT, EQ)
new_esEs6(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs4(x0, x1, ty_Int)
new_esEs6(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs24(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Int)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs14([], :(x0, x1), x2)
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Zero, Succ(x0))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_Bool)
new_primPlusNat0(Zero, Zero)
new_esEs10(True, True)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Double)
new_esEs14([], [], x0)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs26(x0, x1, ty_Char)
new_esEs16(:%(x0, x1), :%(x2, x3), x4)
new_esEs21(x0, x1, ty_Bool)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Double)
new_esEs17(Nothing, Just(x0), x1)
new_esEs5(x0, x1, ty_Ordering)
new_esEs17(Just(x0), Just(x1), ty_Ordering)
new_esEs20(x0, x1, ty_Float)
new_primPlusNat0(Zero, Succ(x0))
new_esEs4(x0, x1, ty_Float)
new_esEs6(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Float)
new_esEs5(x0, x1, ty_Char)
new_esEs24(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Float)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs17(Just(x0), Just(x1), ty_Double)
new_primPlusNat1(Zero, x0)
new_esEs4(x0, x1, ty_Integer)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Int)
new_esEs5(x0, x1, ty_@0)
new_esEs17(Just(x0), Just(x1), ty_Integer)
new_esEs25(x0, x1, ty_@0)
new_esEs4(x0, x1, app(ty_[], x2))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_esEs4(x0, x1, ty_Double)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, ty_Bool)
new_esEs4(x0, x1, ty_@0)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(x0, x1, ty_Char)
new_esEs4(x0, x1, ty_Ordering)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs4(x0, x1, ty_Int)
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(x0, x1, ty_Float)
new_esEs4(x0, x1, ty_Integer)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_[], x2))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                        ↳ QDP
                                          ↳ QDPSizeChangeProof
                                ↳ QDP
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs1(xx20, False, xx22, xx23, be, bf) → new_psPs0(Right(xx20), xx22, xx23, be, bf)
new_psPs0(Right(xx300), :(Left(xx400), xx41), xx5, bc, bd) → new_psPs1(xx300, False, xx41, xx5, bc, bd)
new_psPs0(Right(xx300), :(Right(xx400), xx41), xx5, bc, bd) → new_psPs1(xx300, new_esEs5(xx300, xx400, bd), xx41, xx5, bc, bd)

The TRS R consists of the following rules:

new_esEs5(xx300, xx400, ty_Integer) → new_esEs12(xx300, xx400)
new_esEs5(xx300, xx400, app(ty_[], eh)) → new_esEs14(xx300, xx400, eh)
new_esEs5(xx300, xx400, ty_@0) → new_esEs7(xx300, xx400)
new_esEs5(xx300, xx400, ty_Double) → new_esEs9(xx300, xx400)
new_esEs5(xx300, xx400, app(app(ty_Either, fc), fd)) → new_esEs6(xx300, xx400, fc, fd)
new_esEs5(xx300, xx400, ty_Float) → new_esEs11(xx300, xx400)
new_esEs5(xx300, xx400, app(ty_Ratio, fa)) → new_esEs16(xx300, xx400, fa)
new_esEs5(xx300, xx400, ty_Char) → new_esEs19(xx300, xx400)
new_esEs5(xx300, xx400, ty_Int) → new_esEs15(xx300, xx400)
new_esEs5(xx300, xx400, app(app(app(ty_@3, ff), fg), fh)) → new_esEs18(xx300, xx400, ff, fg, fh)
new_esEs5(xx300, xx400, ty_Bool) → new_esEs10(xx300, xx400)
new_esEs5(xx300, xx400, app(ty_Maybe, fb)) → new_esEs17(xx300, xx400, fb)
new_esEs5(xx300, xx400, ty_Ordering) → new_esEs8(xx300, xx400)
new_esEs5(xx300, xx400, app(app(ty_@2, ef), eg)) → new_esEs13(xx300, xx400, ef, eg)
new_esEs13(@2(xx3000, xx3001), @2(xx4000, xx4001), ga, gb) → new_asAs(new_esEs21(xx3000, xx4000, ga), new_esEs20(xx3001, xx4001, gb))
new_esEs21(xx3000, xx4000, app(ty_Maybe, bag)) → new_esEs17(xx3000, xx4000, bag)
new_esEs21(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(app(ty_Either, bah), bba)) → new_esEs6(xx3000, xx4000, bah, bba)
new_esEs21(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs18(xx3000, xx4000, bbb, bbc, bbd)
new_esEs21(xx3000, xx4000, app(app(ty_@2, bac), bad)) → new_esEs13(xx3000, xx4000, bac, bad)
new_esEs21(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs21(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(ty_Ratio, baf)) → new_esEs16(xx3000, xx4000, baf)
new_esEs21(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs21(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(ty_[], bae)) → new_esEs14(xx3000, xx4000, bae)
new_esEs21(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs21(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs20(xx3001, xx4001, app(ty_Maybe, he)) → new_esEs17(xx3001, xx4001, he)
new_esEs20(xx3001, xx4001, ty_Bool) → new_esEs10(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_Char) → new_esEs19(xx3001, xx4001)
new_esEs20(xx3001, xx4001, app(ty_Ratio, hd)) → new_esEs16(xx3001, xx4001, hd)
new_esEs20(xx3001, xx4001, ty_Float) → new_esEs11(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_@0) → new_esEs7(xx3001, xx4001)
new_esEs20(xx3001, xx4001, app(app(ty_Either, hf), hg)) → new_esEs6(xx3001, xx4001, hf, hg)
new_esEs20(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_Ordering) → new_esEs8(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_Double) → new_esEs9(xx3001, xx4001)
new_esEs20(xx3001, xx4001, app(ty_[], hc)) → new_esEs14(xx3001, xx4001, hc)
new_esEs20(xx3001, xx4001, app(app(ty_@2, ha), hb)) → new_esEs13(xx3001, xx4001, ha, hb)
new_esEs20(xx3001, xx4001, app(app(app(ty_@3, hh), baa), bab)) → new_esEs18(xx3001, xx4001, hh, baa, bab)
new_asAs(False, xx36) → False
new_asAs(True, xx36) → xx36
new_esEs18(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), gf, gg, gh) → new_asAs(new_esEs26(xx3000, xx4000, gf), new_asAs(new_esEs25(xx3001, xx4001, gg), new_esEs24(xx3002, xx4002, gh)))
new_esEs26(xx3000, xx4000, app(ty_Ratio, bff)) → new_esEs16(xx3000, xx4000, bff)
new_esEs26(xx3000, xx4000, app(app(app(ty_@3, bgb), bgc), bgd)) → new_esEs18(xx3000, xx4000, bgb, bgc, bgd)
new_esEs26(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs26(xx3000, xx4000, app(app(ty_@2, bfc), bfd)) → new_esEs13(xx3000, xx4000, bfc, bfd)
new_esEs26(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs26(xx3000, xx4000, app(ty_Maybe, bfg)) → new_esEs17(xx3000, xx4000, bfg)
new_esEs26(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs26(xx3000, xx4000, app(ty_[], bfe)) → new_esEs14(xx3000, xx4000, bfe)
new_esEs26(xx3000, xx4000, app(app(ty_Either, bfh), bga)) → new_esEs6(xx3000, xx4000, bfh, bga)
new_esEs26(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs25(xx3001, xx4001, app(ty_[], bec)) → new_esEs14(xx3001, xx4001, bec)
new_esEs25(xx3001, xx4001, ty_Char) → new_esEs19(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(ty_Maybe, bee)) → new_esEs17(xx3001, xx4001, bee)
new_esEs25(xx3001, xx4001, ty_Bool) → new_esEs10(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(app(ty_Either, bef), beg)) → new_esEs6(xx3001, xx4001, bef, beg)
new_esEs25(xx3001, xx4001, app(ty_Ratio, bed)) → new_esEs16(xx3001, xx4001, bed)
new_esEs25(xx3001, xx4001, ty_Double) → new_esEs9(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_@0) → new_esEs7(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_Ordering) → new_esEs8(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(app(app(ty_@3, beh), bfa), bfb)) → new_esEs18(xx3001, xx4001, beh, bfa, bfb)
new_esEs25(xx3001, xx4001, ty_Float) → new_esEs11(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(app(ty_@2, bea), beb)) → new_esEs13(xx3001, xx4001, bea, beb)
new_esEs24(xx3002, xx4002, app(ty_Maybe, bdc)) → new_esEs17(xx3002, xx4002, bdc)
new_esEs24(xx3002, xx4002, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs18(xx3002, xx4002, bdf, bdg, bdh)
new_esEs24(xx3002, xx4002, ty_Double) → new_esEs9(xx3002, xx4002)
new_esEs24(xx3002, xx4002, app(app(ty_Either, bdd), bde)) → new_esEs6(xx3002, xx4002, bdd, bde)
new_esEs24(xx3002, xx4002, app(app(ty_@2, bcg), bch)) → new_esEs13(xx3002, xx4002, bcg, bch)
new_esEs24(xx3002, xx4002, app(ty_[], bda)) → new_esEs14(xx3002, xx4002, bda)
new_esEs24(xx3002, xx4002, ty_Integer) → new_esEs12(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_Int) → new_esEs15(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_Float) → new_esEs11(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_Char) → new_esEs19(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_Bool) → new_esEs10(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_@0) → new_esEs7(xx3002, xx4002)
new_esEs24(xx3002, xx4002, app(ty_Ratio, bdb)) → new_esEs16(xx3002, xx4002, bdb)
new_esEs24(xx3002, xx4002, ty_Ordering) → new_esEs8(xx3002, xx4002)
new_esEs8(GT, EQ) → False
new_esEs8(EQ, GT) → False
new_esEs8(LT, LT) → True
new_esEs8(GT, GT) → True
new_esEs8(GT, LT) → False
new_esEs8(LT, GT) → False
new_esEs8(EQ, EQ) → True
new_esEs8(EQ, LT) → False
new_esEs8(LT, EQ) → False
new_esEs16(:%(xx3000, xx3001), :%(xx4000, xx4001), gd) → new_asAs(new_esEs23(xx3000, xx4000, gd), new_esEs22(xx3001, xx4001, gd))
new_esEs23(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs23(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs22(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs22(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs15(xx300, xx400) → new_primEqInt(xx300, xx400)
new_primEqInt(Neg(Succ(xx30000)), Pos(xx4000)) → False
new_primEqInt(Pos(Succ(xx30000)), Neg(xx4000)) → False
new_primEqInt(Pos(Zero), Neg(Succ(xx40000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(xx40000))) → False
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_primEqInt(Neg(Succ(xx30000)), Neg(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Succ(xx30000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(xx40000))) → False
new_primEqInt(Pos(Succ(xx30000)), Pos(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_primEqInt(Pos(Zero), Pos(Succ(xx40000))) → False
new_primEqInt(Pos(Succ(xx30000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqNat0(Succ(xx30000), Zero) → False
new_primEqNat0(Zero, Succ(xx40000)) → False
new_primEqNat0(Zero, Zero) → True
new_primEqNat0(Succ(xx30000), Succ(xx40000)) → new_primEqNat0(xx30000, xx40000)
new_esEs12(Integer(xx3000), Integer(xx4000)) → new_primEqInt(xx3000, xx4000)
new_esEs7(@0, @0) → True
new_esEs10(True, True) → True
new_esEs10(False, False) → True
new_esEs10(False, True) → False
new_esEs10(True, False) → False
new_esEs19(Char(xx3000), Char(xx4000)) → new_primEqNat0(xx3000, xx4000)
new_esEs11(Float(xx3000, xx3001), Float(xx4000, xx4001)) → new_esEs15(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_sr(Pos(xx30010), Neg(xx40010)) → Neg(new_primMulNat0(xx30010, xx40010))
new_sr(Neg(xx30010), Pos(xx40010)) → Neg(new_primMulNat0(xx30010, xx40010))
new_sr(Neg(xx30010), Neg(xx40010)) → Pos(new_primMulNat0(xx30010, xx40010))
new_sr(Pos(xx30010), Pos(xx40010)) → Pos(new_primMulNat0(xx30010, xx40010))
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Succ(xx300100), Zero) → Zero
new_primMulNat0(Zero, Succ(xx400100)) → Zero
new_primMulNat0(Succ(xx300100), Succ(xx400100)) → new_primPlusNat1(new_primMulNat0(xx300100, Succ(xx400100)), xx400100)
new_primPlusNat1(Succ(xx370), xx400100) → Succ(Succ(new_primPlusNat0(xx370, xx400100)))
new_primPlusNat1(Zero, xx400100) → Succ(xx400100)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(xx3700), Succ(xx4001000)) → Succ(Succ(new_primPlusNat0(xx3700, xx4001000)))
new_primPlusNat0(Succ(xx3700), Zero) → Succ(xx3700)
new_primPlusNat0(Zero, Succ(xx4001000)) → Succ(xx4001000)
new_esEs14([], [], gc) → True
new_esEs14(:(xx3000, xx3001), :(xx4000, xx4001), gc) → new_asAs(new_esEs27(xx3000, xx4000, gc), new_esEs14(xx3001, xx4001, gc))
new_esEs14(:(xx3000, xx3001), [], gc) → False
new_esEs14([], :(xx4000, xx4001), gc) → False
new_esEs27(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs27(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(ty_Ratio, bgh)) → new_esEs16(xx3000, xx4000, bgh)
new_esEs27(xx3000, xx4000, app(ty_Maybe, bha)) → new_esEs17(xx3000, xx4000, bha)
new_esEs27(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(app(ty_Either, bhb), bhc)) → new_esEs6(xx3000, xx4000, bhb, bhc)
new_esEs27(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs27(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs27(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(app(ty_@2, bge), bgf)) → new_esEs13(xx3000, xx4000, bge, bgf)
new_esEs27(xx3000, xx4000, app(app(app(ty_@3, bhd), bhe), bhf)) → new_esEs18(xx3000, xx4000, bhd, bhe, bhf)
new_esEs27(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(ty_[], bgg)) → new_esEs14(xx3000, xx4000, bgg)
new_esEs27(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), ty_@0, bg) → new_esEs7(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_Ratio, cc), bg) → new_esEs16(xx3000, xx4000, cc)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_Maybe, cd), bg) → new_esEs17(xx3000, xx4000, cd)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_Maybe, bca)) → new_esEs17(xx3000, xx4000, bca)
new_esEs17(Just(xx3000), Just(xx4000), app(app(ty_Either, bcb), bcc)) → new_esEs6(xx3000, xx4000, bcb, bcc)
new_esEs6(Left(xx3000), Left(xx4000), app(app(ty_Either, ce), cf), bg) → new_esEs6(xx3000, xx4000, ce, cf)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(ty_Either, ea), eb)) → new_esEs6(xx3000, xx4000, ea, eb)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_Maybe, dh)) → new_esEs17(xx3000, xx4000, dh)
new_esEs6(Left(xx3000), Left(xx4000), ty_Integer, bg) → new_esEs12(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), ty_Float, bg) → new_esEs11(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), ty_Char, bg) → new_esEs19(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_[], df)) → new_esEs14(xx3000, xx4000, df)
new_esEs6(Left(xx3000), Left(xx4000), ty_Ordering, bg) → new_esEs8(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(ty_@2, dd), de)) → new_esEs13(xx3000, xx4000, dd, de)
new_esEs6(Left(xx3000), Left(xx4000), ty_Double, bg) → new_esEs9(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs6(Left(xx3000), Right(xx4000), dc, bg) → False
new_esEs6(Right(xx3000), Left(xx4000), dc, bg) → False
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(app(app(ty_@3, cg), da), db), bg) → new_esEs18(xx3000, xx4000, cg, da, db)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_Ratio, dg)) → new_esEs16(xx3000, xx4000, dg)
new_esEs6(Left(xx3000), Left(xx4000), app(app(ty_@2, bh), ca), bg) → new_esEs13(xx3000, xx4000, bh, ca)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), ty_Int, bg) → new_esEs15(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_[], cb), bg) → new_esEs14(xx3000, xx4000, cb)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(app(ty_@3, ec), ed), ee)) → new_esEs18(xx3000, xx4000, ec, ed, ee)
new_esEs6(Left(xx3000), Left(xx4000), ty_Bool, bg) → new_esEs10(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs9(Double(xx3000, xx3001), Double(xx4000, xx4001)) → new_esEs15(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_esEs17(Just(xx3000), Just(xx4000), app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs18(xx3000, xx4000, bcd, bce, bcf)
new_esEs17(Just(xx3000), Just(xx4000), ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_Ratio, bbh)) → new_esEs16(xx3000, xx4000, bbh)
new_esEs17(Just(xx3000), Just(xx4000), ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), app(app(ty_@2, bbe), bbf)) → new_esEs13(xx3000, xx4000, bbe, bbf)
new_esEs17(Just(xx3000), Just(xx4000), ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs17(Nothing, Nothing, ge) → True
new_esEs17(Just(xx3000), Just(xx4000), ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs17(Just(xx3000), Nothing, ge) → False
new_esEs17(Nothing, Just(xx4000), ge) → False
new_esEs17(Just(xx3000), Just(xx4000), ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_[], bbg)) → new_esEs14(xx3000, xx4000, bbg)

The set Q consists of the following terms:

new_esEs6(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs27(x0, x1, ty_@0)
new_esEs17(Nothing, Nothing, x0)
new_esEs6(Right(x0), Right(x1), x2, ty_Char)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs7(@0, @0)
new_primMulNat0(Succ(x0), Zero)
new_esEs21(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Char)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs27(x0, x1, ty_Bool)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs18(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Char)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Bool)
new_esEs6(Right(x0), Right(x1), x2, ty_Int)
new_primEqNat0(Succ(x0), Zero)
new_esEs22(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs14(:(x0, x1), [], x2)
new_esEs8(EQ, EQ)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Double)
new_esEs15(x0, x1)
new_esEs6(Right(x0), Right(x1), x2, ty_Double)
new_esEs21(x0, x1, ty_Ordering)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(x0, x1, ty_Int)
new_esEs17(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs5(x0, x1, ty_Float)
new_esEs11(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, ty_Float)
new_asAs(True, x0)
new_primMulNat0(Zero, Succ(x0))
new_esEs6(Left(x0), Left(x1), ty_Float, x2)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(Integer(x0), Integer(x1))
new_esEs24(x0, x1, ty_Double)
new_esEs8(GT, GT)
new_esEs25(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), ty_Integer, x2)
new_esEs6(Left(x0), Left(x1), ty_Int, x2)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs17(Just(x0), Just(x1), ty_Float)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, ty_@0)
new_esEs6(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs6(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs27(x0, x1, ty_Int)
new_esEs17(Just(x0), Just(x1), app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs8(LT, LT)
new_esEs27(x0, x1, ty_Char)
new_esEs17(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs14(:(x0, x1), :(x2, x3), x4)
new_esEs17(Just(x0), Just(x1), ty_Int)
new_esEs6(Left(x0), Left(x1), ty_@0, x2)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_sr(Neg(x0), Neg(x1))
new_esEs9(Double(x0, x1), Double(x2, x3))
new_primPlusNat0(Succ(x0), Zero)
new_esEs8(GT, EQ)
new_esEs8(EQ, GT)
new_esEs21(x0, x1, ty_Char)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs19(Char(x0), Char(x1))
new_esEs6(Right(x0), Right(x1), x2, ty_Integer)
new_esEs26(x0, x1, ty_Float)
new_esEs20(x0, x1, app(ty_[], x2))
new_sr(Pos(x0), Pos(x1))
new_esEs5(x0, x1, ty_Bool)
new_esEs6(Left(x0), Left(x1), ty_Char, x2)
new_esEs20(x0, x1, ty_Integer)
new_esEs8(LT, GT)
new_esEs8(GT, LT)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs27(x0, x1, ty_Double)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Integer)
new_esEs17(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs10(False, False)
new_esEs20(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Float)
new_esEs20(x0, x1, ty_Int)
new_primEqNat0(Zero, Zero)
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs25(x0, x1, ty_Ordering)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Ordering)
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_@0)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs26(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs17(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Right(x0), Right(x1), x2, ty_@0)
new_esEs6(Left(x0), Left(x1), ty_Double, x2)
new_esEs26(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_primMulNat0(Zero, Zero)
new_esEs26(x0, x1, ty_Ordering)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Ordering)
new_esEs6(Right(x0), Left(x1), x2, x3)
new_esEs6(Left(x0), Right(x1), x2, x3)
new_esEs17(Just(x0), Just(x1), ty_Char)
new_esEs23(x0, x1, ty_Integer)
new_asAs(False, x0)
new_primPlusNat1(Succ(x0), x1)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Int)
new_esEs17(Just(x0), Nothing, x1)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs13(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs25(x0, x1, ty_Float)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs20(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs6(Left(x0), Left(x1), ty_Bool, x2)
new_esEs17(Just(x0), Just(x1), ty_@0)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs25(x0, x1, ty_Double)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs17(Just(x0), Just(x1), ty_Bool)
new_esEs17(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_@0)
new_esEs8(EQ, LT)
new_esEs8(LT, EQ)
new_esEs6(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs6(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs24(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Int)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs14([], :(x0, x1), x2)
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Zero, Succ(x0))
new_esEs26(x0, x1, ty_Bool)
new_primPlusNat0(Zero, Zero)
new_esEs10(True, True)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Double)
new_esEs14([], [], x0)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs26(x0, x1, ty_Char)
new_esEs16(:%(x0, x1), :%(x2, x3), x4)
new_esEs21(x0, x1, ty_Bool)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Double)
new_esEs17(Nothing, Just(x0), x1)
new_esEs5(x0, x1, ty_Ordering)
new_esEs17(Just(x0), Just(x1), ty_Ordering)
new_esEs20(x0, x1, ty_Float)
new_primPlusNat0(Zero, Succ(x0))
new_esEs6(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Float)
new_esEs5(x0, x1, ty_Char)
new_esEs24(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Float)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs17(Just(x0), Just(x1), ty_Double)
new_primPlusNat1(Zero, x0)
new_esEs26(x0, x1, ty_Int)
new_esEs5(x0, x1, ty_@0)
new_esEs17(Just(x0), Just(x1), ty_Integer)
new_esEs25(x0, x1, ty_@0)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                ↳ QDP
                                  ↳ UsableRulesProof
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs0(Left(xx300), :(Right(xx400), xx41), xx5, bc, bd) → new_psPs(xx300, False, xx41, xx5, bc, bd)
new_psPs(xx11, False, xx13, xx14, ba, bb) → new_psPs0(Left(xx11), xx13, xx14, ba, bb)
new_psPs0(Left(xx300), :(Left(xx400), xx41), xx5, bc, bd) → new_psPs(xx300, new_esEs4(xx300, xx400, bc), xx41, xx5, bc, bd)

The TRS R consists of the following rules:

new_esEs25(xx3001, xx4001, app(ty_[], bec)) → new_esEs14(xx3001, xx4001, bec)
new_esEs25(xx3001, xx4001, ty_Char) → new_esEs19(xx3001, xx4001)
new_esEs27(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs20(xx3001, xx4001, app(ty_Maybe, he)) → new_esEs17(xx3001, xx4001, he)
new_esEs27(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs25(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Bool) → new_esEs10(xx3000, xx4000)
new_primEqInt(Neg(Succ(xx30000)), Pos(xx4000)) → False
new_primEqInt(Pos(Succ(xx30000)), Neg(xx4000)) → False
new_esEs5(xx300, xx400, ty_Integer) → new_esEs12(xx300, xx400)
new_esEs16(:%(xx3000, xx3001), :%(xx4000, xx4001), gd) → new_asAs(new_esEs23(xx3000, xx4000, gd), new_esEs22(xx3001, xx4001, gd))
new_esEs26(xx3000, xx4000, app(ty_Ratio, bff)) → new_esEs16(xx3000, xx4000, bff)
new_primEqInt(Pos(Zero), Neg(Succ(xx40000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(xx40000))) → False
new_esEs6(Left(xx3000), Left(xx4000), ty_@0, bg) → new_esEs7(xx3000, xx4000)
new_esEs5(xx300, xx400, app(ty_[], eh)) → new_esEs14(xx300, xx400, eh)
new_esEs25(xx3001, xx4001, app(ty_Maybe, bee)) → new_esEs17(xx3001, xx4001, bee)
new_esEs24(xx3002, xx4002, app(ty_Maybe, bdc)) → new_esEs17(xx3002, xx4002, bdc)
new_esEs5(xx300, xx400, ty_@0) → new_esEs7(xx300, xx400)
new_esEs20(xx3001, xx4001, ty_Bool) → new_esEs10(xx3001, xx4001)
new_esEs8(GT, EQ) → False
new_esEs8(EQ, GT) → False
new_esEs20(xx3001, xx4001, ty_Char) → new_esEs19(xx3001, xx4001)
new_esEs24(xx3002, xx4002, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs18(xx3002, xx4002, bdf, bdg, bdh)
new_esEs17(Just(xx3000), Just(xx4000), app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs18(xx3000, xx4000, bcd, bce, bcf)
new_primMulNat0(Zero, Zero) → Zero
new_esEs27(xx3000, xx4000, app(ty_Ratio, bgh)) → new_esEs16(xx3000, xx4000, bgh)
new_esEs25(xx3001, xx4001, ty_Bool) → new_esEs10(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(app(ty_Either, bef), beg)) → new_esEs6(xx3001, xx4001, bef, beg)
new_esEs5(xx300, xx400, ty_Double) → new_esEs9(xx300, xx400)
new_esEs6(Left(xx3000), Left(xx4000), app(app(ty_Either, ce), cf), bg) → new_esEs6(xx3000, xx4000, ce, cf)
new_esEs4(xx300, xx400, ty_Ordering) → new_esEs8(xx300, xx400)
new_esEs5(xx300, xx400, app(app(ty_Either, fc), fd)) → new_esEs6(xx300, xx400, fc, fd)
new_esEs20(xx3001, xx4001, app(ty_Ratio, hd)) → new_esEs16(xx3001, xx4001, hd)
new_esEs24(xx3002, xx4002, ty_Double) → new_esEs9(xx3002, xx4002)
new_esEs17(Just(xx3000), Just(xx4000), ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_Ratio, cc), bg) → new_esEs16(xx3000, xx4000, cc)
new_esEs27(xx3000, xx4000, app(ty_Maybe, bha)) → new_esEs17(xx3000, xx4000, bha)
new_esEs26(xx3000, xx4000, app(app(app(ty_@3, bgb), bgc), bgd)) → new_esEs18(xx3000, xx4000, bgb, bgc, bgd)
new_esEs24(xx3002, xx4002, app(app(ty_Either, bdd), bde)) → new_esEs6(xx3002, xx4002, bdd, bde)
new_esEs27(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs24(xx3002, xx4002, app(app(ty_@2, bcg), bch)) → new_esEs13(xx3002, xx4002, bcg, bch)
new_esEs17(Just(xx3000), Just(xx4000), ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(ty_Maybe, bag)) → new_esEs17(xx3000, xx4000, bag)
new_esEs25(xx3001, xx4001, app(ty_Ratio, bed)) → new_esEs16(xx3001, xx4001, bed)
new_esEs24(xx3002, xx4002, app(ty_[], bda)) → new_esEs14(xx3002, xx4002, bda)
new_esEs26(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs5(xx300, xx400, ty_Float) → new_esEs11(xx300, xx400)
new_esEs24(xx3002, xx4002, ty_Integer) → new_esEs12(xx3002, xx4002)
new_sr(Pos(xx30010), Neg(xx40010)) → Neg(new_primMulNat0(xx30010, xx40010))
new_sr(Neg(xx30010), Pos(xx40010)) → Neg(new_primMulNat0(xx30010, xx40010))
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs20(xx3001, xx4001, ty_Float) → new_esEs11(xx3001, xx4001)
new_esEs27(xx3000, xx4000, app(app(ty_Either, bhb), bhc)) → new_esEs6(xx3000, xx4000, bhb, bhc)
new_esEs21(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs5(xx300, xx400, app(ty_Ratio, fa)) → new_esEs16(xx300, xx400, fa)
new_esEs24(xx3002, xx4002, ty_Int) → new_esEs15(xx3002, xx4002)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_Maybe, dh)) → new_esEs17(xx3000, xx4000, dh)
new_esEs4(xx300, xx400, ty_Float) → new_esEs11(xx300, xx400)
new_esEs27(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs4(xx300, xx400, app(app(ty_@2, ga), gb)) → new_esEs13(xx300, xx400, ga, gb)
new_esEs23(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(app(ty_Either, bah), bba)) → new_esEs6(xx3000, xx4000, bah, bba)
new_esEs27(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs12(Integer(xx3000), Integer(xx4000)) → new_primEqInt(xx3000, xx4000)
new_esEs10(True, True) → True
new_esEs26(xx3000, xx4000, app(app(ty_@2, bfc), bfd)) → new_esEs13(xx3000, xx4000, bfc, bfd)
new_esEs4(xx300, xx400, app(ty_Maybe, ge)) → new_esEs17(xx300, xx400, ge)
new_esEs4(xx300, xx400, app(app(app(ty_@3, gf), gg), gh)) → new_esEs18(xx300, xx400, gf, gg, gh)
new_esEs6(Left(xx3000), Left(xx4000), ty_Integer, bg) → new_esEs12(xx3000, xx4000)
new_primEqNat0(Succ(xx30000), Zero) → False
new_primEqNat0(Zero, Succ(xx40000)) → False
new_esEs6(Left(xx3000), Left(xx4000), ty_Float, bg) → new_esEs11(xx3000, xx4000)
new_primPlusNat0(Zero, Zero) → Zero
new_esEs20(xx3001, xx4001, ty_@0) → new_esEs7(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_Double) → new_esEs9(xx3001, xx4001)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs25(xx3001, xx4001, ty_@0) → new_esEs7(xx3001, xx4001)
new_esEs26(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs14([], [], gc) → True
new_esEs27(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_Ratio, bbh)) → new_esEs16(xx3000, xx4000, bbh)
new_esEs6(Left(xx3000), Left(xx4000), ty_Char, bg) → new_esEs19(xx3000, xx4000)
new_esEs20(xx3001, xx4001, app(app(ty_Either, hf), hg)) → new_esEs6(xx3001, xx4001, hf, hg)
new_esEs15(xx300, xx400) → new_primEqInt(xx300, xx400)
new_primPlusNat1(Succ(xx370), xx400100) → Succ(Succ(new_primPlusNat0(xx370, xx400100)))
new_esEs22(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_[], df)) → new_esEs14(xx3000, xx4000, df)
new_esEs6(Left(xx3000), Left(xx4000), ty_Ordering, bg) → new_esEs8(xx3000, xx4000)
new_esEs4(xx300, xx400, ty_Char) → new_esEs19(xx300, xx400)
new_esEs26(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(ty_@2, dd), de)) → new_esEs13(xx3000, xx4000, dd, de)
new_esEs6(Left(xx3000), Left(xx4000), ty_Double, bg) → new_esEs9(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs19(Char(xx3000), Char(xx4000)) → new_primEqNat0(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(app(ty_@2, bge), bgf)) → new_esEs13(xx3000, xx4000, bge, bgf)
new_esEs8(LT, LT) → True
new_esEs6(Left(xx3000), Right(xx4000), dc, bg) → False
new_esEs6(Right(xx3000), Left(xx4000), dc, bg) → False
new_esEs21(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs18(xx3000, xx4000, bbb, bbc, bbd)
new_esEs25(xx3001, xx4001, ty_Ordering) → new_esEs8(xx3001, xx4001)
new_sr(Neg(xx30010), Neg(xx40010)) → Pos(new_primMulNat0(xx30010, xx40010))
new_esEs21(xx3000, xx4000, app(app(ty_@2, bac), bad)) → new_esEs13(xx3000, xx4000, bac, bad)
new_esEs17(Just(xx3000), Just(xx4000), ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(app(app(ty_@3, cg), da), db), bg) → new_esEs18(xx3000, xx4000, cg, da, db)
new_asAs(False, xx36) → False
new_sr(Pos(xx30010), Pos(xx40010)) → Pos(new_primMulNat0(xx30010, xx40010))
new_esEs11(Float(xx3000, xx3001), Float(xx4000, xx4001)) → new_esEs15(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_primEqNat0(Zero, Zero) → True
new_esEs26(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_primMulNat0(Succ(xx300100), Zero) → Zero
new_primMulNat0(Zero, Succ(xx400100)) → Zero
new_esEs14(:(xx3000, xx3001), :(xx4000, xx4001), gc) → new_asAs(new_esEs27(xx3000, xx4000, gc), new_esEs14(xx3001, xx4001, gc))
new_esEs5(xx300, xx400, ty_Char) → new_esEs19(xx300, xx400)
new_esEs4(xx300, xx400, ty_Bool) → new_esEs10(xx300, xx400)
new_primMulNat0(Succ(xx300100), Succ(xx400100)) → new_primPlusNat1(new_primMulNat0(xx300100, Succ(xx400100)), xx400100)
new_esEs17(Just(xx3000), Just(xx4000), app(app(ty_@2, bbe), bbf)) → new_esEs13(xx3000, xx4000, bbe, bbf)
new_esEs21(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_Ratio, dg)) → new_esEs16(xx3000, xx4000, dg)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(ty_Either, ea), eb)) → new_esEs6(xx3000, xx4000, ea, eb)
new_esEs25(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs17(Just(xx3000), Just(xx4000), app(app(ty_Either, bcb), bcc)) → new_esEs6(xx3000, xx4000, bcb, bcc)
new_esEs24(xx3002, xx4002, ty_Float) → new_esEs11(xx3002, xx4002)
new_esEs4(xx300, xx400, ty_Integer) → new_esEs12(xx300, xx400)
new_esEs26(xx3000, xx4000, app(ty_Maybe, bfg)) → new_esEs17(xx3000, xx4000, bfg)
new_esEs4(xx300, xx400, ty_Double) → new_esEs9(xx300, xx400)
new_esEs4(xx300, xx400, app(ty_[], gc)) → new_esEs14(xx300, xx400, gc)
new_esEs21(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs24(xx3002, xx4002, ty_Char) → new_esEs19(xx3002, xx4002)
new_esEs8(GT, GT) → True
new_esEs4(xx300, xx400, app(app(ty_Either, dc), bg)) → new_esEs6(xx300, xx400, dc, bg)
new_esEs6(Left(xx3000), Left(xx4000), app(app(ty_@2, bh), ca), bg) → new_esEs13(xx3000, xx4000, bh, ca)
new_esEs20(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs26(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs8(GT, LT) → False
new_esEs8(LT, GT) → False
new_esEs21(xx3000, xx4000, app(ty_Ratio, baf)) → new_esEs16(xx3000, xx4000, baf)
new_esEs5(xx300, xx400, ty_Int) → new_esEs15(xx300, xx400)
new_esEs25(xx3001, xx4001, app(app(app(ty_@3, beh), bfa), bfb)) → new_esEs18(xx3001, xx4001, beh, bfa, bfb)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(app(app(ty_@3, bhd), bhe), bhf)) → new_esEs18(xx3000, xx4000, bhd, bhe, bhf)
new_esEs6(Left(xx3000), Left(xx4000), ty_Int, bg) → new_esEs15(xx3000, xx4000)
new_esEs13(@2(xx3000, xx3001), @2(xx4000, xx4001), ga, gb) → new_asAs(new_esEs21(xx3000, xx4000, ga), new_esEs20(xx3001, xx4001, gb))
new_primEqInt(Neg(Succ(xx30000)), Neg(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_esEs20(xx3001, xx4001, ty_Ordering) → new_esEs8(xx3001, xx4001)
new_esEs23(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs27(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs22(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs17(Just(xx3000), Just(xx4000), ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs20(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_[], cb), bg) → new_esEs14(xx3000, xx4000, cb)
new_esEs14(:(xx3000, xx3001), [], gc) → False
new_esEs14([], :(xx4000, xx4001), gc) → False
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(app(ty_@3, ec), ed), ee)) → new_esEs18(xx3000, xx4000, ec, ed, ee)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs24(xx3002, xx4002, ty_Bool) → new_esEs10(xx3002, xx4002)
new_esEs26(xx3000, xx4000, app(ty_[], bfe)) → new_esEs14(xx3000, xx4000, bfe)
new_esEs6(Left(xx3000), Left(xx4000), ty_Bool, bg) → new_esEs10(xx3000, xx4000)
new_primEqInt(Neg(Succ(xx30000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(xx40000))) → False
new_esEs8(EQ, EQ) → True
new_esEs17(Nothing, Nothing, ge) → True
new_esEs21(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_primPlusNat1(Zero, xx400100) → Succ(xx400100)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_Maybe, cd), bg) → new_esEs17(xx3000, xx4000, cd)
new_primPlusNat0(Succ(xx3700), Succ(xx4001000)) → Succ(Succ(new_primPlusNat0(xx3700, xx4001000)))
new_esEs26(xx3000, xx4000, app(app(ty_Either, bfh), bga)) → new_esEs6(xx3000, xx4000, bfh, bga)
new_esEs17(Just(xx3000), Just(xx4000), ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs10(False, False) → True
new_esEs27(xx3000, xx4000, app(ty_[], bgg)) → new_esEs14(xx3000, xx4000, bgg)
new_esEs5(xx300, xx400, app(app(app(ty_@3, ff), fg), fh)) → new_esEs18(xx300, xx400, ff, fg, fh)
new_esEs4(xx300, xx400, ty_Int) → new_esEs15(xx300, xx400)
new_asAs(True, xx36) → xx36
new_esEs20(xx3001, xx4001, ty_Double) → new_esEs9(xx3001, xx4001)
new_esEs4(xx300, xx400, ty_@0) → new_esEs7(xx300, xx400)
new_esEs10(False, True) → False
new_esEs10(True, False) → False
new_esEs25(xx3001, xx4001, ty_Float) → new_esEs11(xx3001, xx4001)
new_esEs24(xx3002, xx4002, ty_@0) → new_esEs7(xx3002, xx4002)
new_esEs17(Just(xx3000), Just(xx4000), ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs9(Double(xx3000, xx3001), Double(xx4000, xx4001)) → new_esEs15(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_primEqInt(Pos(Succ(xx30000)), Pos(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_esEs5(xx300, xx400, ty_Bool) → new_esEs10(xx300, xx400)
new_esEs24(xx3002, xx4002, app(ty_Ratio, bdb)) → new_esEs16(xx3002, xx4002, bdb)
new_esEs5(xx300, xx400, app(ty_Maybe, fb)) → new_esEs17(xx300, xx400, fb)
new_esEs17(Just(xx3000), Nothing, ge) → False
new_esEs17(Nothing, Just(xx4000), ge) → False
new_esEs20(xx3001, xx4001, app(ty_[], hc)) → new_esEs14(xx3001, xx4001, hc)
new_esEs21(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs5(xx300, xx400, ty_Ordering) → new_esEs8(xx300, xx400)
new_primEqNat0(Succ(xx30000), Succ(xx40000)) → new_primEqNat0(xx30000, xx40000)
new_esEs27(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(ty_[], bae)) → new_esEs14(xx3000, xx4000, bae)
new_esEs25(xx3001, xx4001, app(app(ty_@2, bea), beb)) → new_esEs13(xx3001, xx4001, bea, beb)
new_esEs21(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs7(@0, @0) → True
new_esEs20(xx3001, xx4001, app(app(ty_@2, ha), hb)) → new_esEs13(xx3001, xx4001, ha, hb)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_Maybe, bca)) → new_esEs17(xx3000, xx4000, bca)
new_esEs24(xx3002, xx4002, ty_Ordering) → new_esEs8(xx3002, xx4002)
new_esEs4(xx300, xx400, app(ty_Ratio, gd)) → new_esEs16(xx300, xx400, gd)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs18(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), gf, gg, gh) → new_asAs(new_esEs26(xx3000, xx4000, gf), new_asAs(new_esEs25(xx3001, xx4001, gg), new_esEs24(xx3002, xx4002, gh)))
new_esEs8(EQ, LT) → False
new_esEs8(LT, EQ) → False
new_primEqInt(Pos(Zero), Pos(Succ(xx40000))) → False
new_primEqInt(Pos(Succ(xx30000)), Pos(Zero)) → False
new_esEs21(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs5(xx300, xx400, app(app(ty_@2, ef), eg)) → new_esEs13(xx300, xx400, ef, eg)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primPlusNat0(Succ(xx3700), Zero) → Succ(xx3700)
new_primPlusNat0(Zero, Succ(xx4001000)) → Succ(xx4001000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_[], bbg)) → new_esEs14(xx3000, xx4000, bbg)
new_esEs20(xx3001, xx4001, app(app(app(ty_@3, hh), baa), bab)) → new_esEs18(xx3001, xx4001, hh, baa, bab)

The set Q consists of the following terms:

new_esEs6(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs27(x0, x1, ty_@0)
new_esEs17(Nothing, Nothing, x0)
new_esEs6(Right(x0), Right(x1), x2, ty_Char)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs7(@0, @0)
new_primMulNat0(Succ(x0), Zero)
new_esEs21(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Char)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs27(x0, x1, ty_Bool)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs4(x0, x1, ty_Double)
new_esEs18(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Char)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Bool)
new_esEs6(Right(x0), Right(x1), x2, ty_Int)
new_primEqNat0(Succ(x0), Zero)
new_esEs22(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs14(:(x0, x1), [], x2)
new_esEs8(EQ, EQ)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Double)
new_esEs15(x0, x1)
new_esEs6(Right(x0), Right(x1), x2, ty_Double)
new_esEs21(x0, x1, ty_Ordering)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(x0, x1, ty_Int)
new_esEs17(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs5(x0, x1, ty_Float)
new_esEs11(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, ty_Float)
new_asAs(True, x0)
new_primMulNat0(Zero, Succ(x0))
new_esEs6(Left(x0), Left(x1), ty_Float, x2)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(Integer(x0), Integer(x1))
new_esEs24(x0, x1, ty_Double)
new_esEs8(GT, GT)
new_esEs25(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), ty_Integer, x2)
new_esEs6(Left(x0), Left(x1), ty_Int, x2)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs17(Just(x0), Just(x1), ty_Float)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, ty_@0)
new_esEs6(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs6(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs27(x0, x1, ty_Int)
new_esEs17(Just(x0), Just(x1), app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs8(LT, LT)
new_esEs27(x0, x1, ty_Char)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs17(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs14(:(x0, x1), :(x2, x3), x4)
new_esEs17(Just(x0), Just(x1), ty_Int)
new_esEs6(Left(x0), Left(x1), ty_@0, x2)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_sr(Neg(x0), Neg(x1))
new_esEs9(Double(x0, x1), Double(x2, x3))
new_primPlusNat0(Succ(x0), Zero)
new_esEs8(GT, EQ)
new_esEs8(EQ, GT)
new_esEs21(x0, x1, ty_Char)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs19(Char(x0), Char(x1))
new_esEs6(Right(x0), Right(x1), x2, ty_Integer)
new_esEs26(x0, x1, ty_Float)
new_esEs20(x0, x1, app(ty_[], x2))
new_sr(Pos(x0), Pos(x1))
new_esEs5(x0, x1, ty_Bool)
new_esEs6(Left(x0), Left(x1), ty_Char, x2)
new_esEs20(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Bool)
new_esEs8(LT, GT)
new_esEs8(GT, LT)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs27(x0, x1, ty_Double)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Integer)
new_esEs17(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs10(False, False)
new_esEs20(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Float)
new_esEs20(x0, x1, ty_Int)
new_primEqNat0(Zero, Zero)
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs25(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_@0)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Ordering)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_@0)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs26(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs17(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Right(x0), Right(x1), x2, ty_@0)
new_esEs6(Left(x0), Left(x1), ty_Double, x2)
new_esEs26(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_primMulNat0(Zero, Zero)
new_esEs26(x0, x1, ty_Ordering)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Ordering)
new_esEs6(Right(x0), Left(x1), x2, x3)
new_esEs6(Left(x0), Right(x1), x2, x3)
new_esEs17(Just(x0), Just(x1), ty_Char)
new_esEs23(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Char)
new_asAs(False, x0)
new_primPlusNat1(Succ(x0), x1)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Int)
new_esEs17(Just(x0), Nothing, x1)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs13(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs4(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Float)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs20(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs6(Left(x0), Left(x1), ty_Bool, x2)
new_esEs17(Just(x0), Just(x1), ty_@0)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs25(x0, x1, ty_Double)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs17(Just(x0), Just(x1), ty_Bool)
new_esEs17(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_@0)
new_esEs8(EQ, LT)
new_esEs8(LT, EQ)
new_esEs6(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs4(x0, x1, ty_Int)
new_esEs6(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs24(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Int)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs14([], :(x0, x1), x2)
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Zero, Succ(x0))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_Bool)
new_primPlusNat0(Zero, Zero)
new_esEs10(True, True)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Double)
new_esEs14([], [], x0)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs26(x0, x1, ty_Char)
new_esEs16(:%(x0, x1), :%(x2, x3), x4)
new_esEs21(x0, x1, ty_Bool)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Double)
new_esEs17(Nothing, Just(x0), x1)
new_esEs5(x0, x1, ty_Ordering)
new_esEs17(Just(x0), Just(x1), ty_Ordering)
new_esEs20(x0, x1, ty_Float)
new_primPlusNat0(Zero, Succ(x0))
new_esEs4(x0, x1, ty_Float)
new_esEs6(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Float)
new_esEs5(x0, x1, ty_Char)
new_esEs24(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Float)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs17(Just(x0), Just(x1), ty_Double)
new_primPlusNat1(Zero, x0)
new_esEs4(x0, x1, ty_Integer)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Int)
new_esEs5(x0, x1, ty_@0)
new_esEs17(Just(x0), Just(x1), ty_Integer)
new_esEs25(x0, x1, ty_@0)
new_esEs4(x0, x1, app(ty_[], x2))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs0(Left(xx300), :(Right(xx400), xx41), xx5, bc, bd) → new_psPs(xx300, False, xx41, xx5, bc, bd)
new_psPs(xx11, False, xx13, xx14, ba, bb) → new_psPs0(Left(xx11), xx13, xx14, ba, bb)
new_psPs0(Left(xx300), :(Left(xx400), xx41), xx5, bc, bd) → new_psPs(xx300, new_esEs4(xx300, xx400, bc), xx41, xx5, bc, bd)

The TRS R consists of the following rules:

new_esEs4(xx300, xx400, ty_Ordering) → new_esEs8(xx300, xx400)
new_esEs4(xx300, xx400, ty_Float) → new_esEs11(xx300, xx400)
new_esEs4(xx300, xx400, app(app(ty_@2, ga), gb)) → new_esEs13(xx300, xx400, ga, gb)
new_esEs4(xx300, xx400, app(ty_Maybe, ge)) → new_esEs17(xx300, xx400, ge)
new_esEs4(xx300, xx400, app(app(app(ty_@3, gf), gg), gh)) → new_esEs18(xx300, xx400, gf, gg, gh)
new_esEs4(xx300, xx400, ty_Char) → new_esEs19(xx300, xx400)
new_esEs4(xx300, xx400, ty_Bool) → new_esEs10(xx300, xx400)
new_esEs4(xx300, xx400, ty_Integer) → new_esEs12(xx300, xx400)
new_esEs4(xx300, xx400, ty_Double) → new_esEs9(xx300, xx400)
new_esEs4(xx300, xx400, app(ty_[], gc)) → new_esEs14(xx300, xx400, gc)
new_esEs4(xx300, xx400, app(app(ty_Either, dc), bg)) → new_esEs6(xx300, xx400, dc, bg)
new_esEs4(xx300, xx400, ty_Int) → new_esEs15(xx300, xx400)
new_esEs4(xx300, xx400, ty_@0) → new_esEs7(xx300, xx400)
new_esEs4(xx300, xx400, app(ty_Ratio, gd)) → new_esEs16(xx300, xx400, gd)
new_esEs16(:%(xx3000, xx3001), :%(xx4000, xx4001), gd) → new_asAs(new_esEs23(xx3000, xx4000, gd), new_esEs22(xx3001, xx4001, gd))
new_esEs23(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs23(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs22(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs22(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_asAs(False, xx36) → False
new_asAs(True, xx36) → xx36
new_esEs15(xx300, xx400) → new_primEqInt(xx300, xx400)
new_primEqInt(Neg(Succ(xx30000)), Pos(xx4000)) → False
new_primEqInt(Pos(Succ(xx30000)), Neg(xx4000)) → False
new_primEqInt(Pos(Zero), Neg(Succ(xx40000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(xx40000))) → False
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_primEqInt(Neg(Succ(xx30000)), Neg(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Succ(xx30000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(xx40000))) → False
new_primEqInt(Pos(Succ(xx30000)), Pos(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_primEqInt(Pos(Zero), Pos(Succ(xx40000))) → False
new_primEqInt(Pos(Succ(xx30000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqNat0(Succ(xx30000), Zero) → False
new_primEqNat0(Zero, Succ(xx40000)) → False
new_primEqNat0(Zero, Zero) → True
new_primEqNat0(Succ(xx30000), Succ(xx40000)) → new_primEqNat0(xx30000, xx40000)
new_esEs12(Integer(xx3000), Integer(xx4000)) → new_primEqInt(xx3000, xx4000)
new_esEs7(@0, @0) → True
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), ty_@0, bg) → new_esEs7(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_Ratio, cc), bg) → new_esEs16(xx3000, xx4000, cc)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_Maybe, cd), bg) → new_esEs17(xx3000, xx4000, cd)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_Maybe, bca)) → new_esEs17(xx3000, xx4000, bca)
new_esEs17(Just(xx3000), Just(xx4000), app(app(ty_Either, bcb), bcc)) → new_esEs6(xx3000, xx4000, bcb, bcc)
new_esEs6(Left(xx3000), Left(xx4000), app(app(ty_Either, ce), cf), bg) → new_esEs6(xx3000, xx4000, ce, cf)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(ty_Either, ea), eb)) → new_esEs6(xx3000, xx4000, ea, eb)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_Maybe, dh)) → new_esEs17(xx3000, xx4000, dh)
new_esEs6(Left(xx3000), Left(xx4000), ty_Integer, bg) → new_esEs12(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), ty_Float, bg) → new_esEs11(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), ty_Char, bg) → new_esEs19(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_[], df)) → new_esEs14(xx3000, xx4000, df)
new_esEs6(Left(xx3000), Left(xx4000), ty_Ordering, bg) → new_esEs8(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(ty_@2, dd), de)) → new_esEs13(xx3000, xx4000, dd, de)
new_esEs6(Left(xx3000), Left(xx4000), ty_Double, bg) → new_esEs9(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs6(Left(xx3000), Right(xx4000), dc, bg) → False
new_esEs6(Right(xx3000), Left(xx4000), dc, bg) → False
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(app(app(ty_@3, cg), da), db), bg) → new_esEs18(xx3000, xx4000, cg, da, db)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_Ratio, dg)) → new_esEs16(xx3000, xx4000, dg)
new_esEs6(Left(xx3000), Left(xx4000), app(app(ty_@2, bh), ca), bg) → new_esEs13(xx3000, xx4000, bh, ca)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), ty_Int, bg) → new_esEs15(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_[], cb), bg) → new_esEs14(xx3000, xx4000, cb)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(app(ty_@3, ec), ed), ee)) → new_esEs18(xx3000, xx4000, ec, ed, ee)
new_esEs6(Left(xx3000), Left(xx4000), ty_Bool, bg) → new_esEs10(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs8(GT, EQ) → False
new_esEs8(EQ, GT) → False
new_esEs8(LT, LT) → True
new_esEs8(GT, GT) → True
new_esEs8(GT, LT) → False
new_esEs8(LT, GT) → False
new_esEs8(EQ, EQ) → True
new_esEs8(EQ, LT) → False
new_esEs8(LT, EQ) → False
new_esEs10(True, True) → True
new_esEs10(False, False) → True
new_esEs10(False, True) → False
new_esEs10(True, False) → False
new_esEs18(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), gf, gg, gh) → new_asAs(new_esEs26(xx3000, xx4000, gf), new_asAs(new_esEs25(xx3001, xx4001, gg), new_esEs24(xx3002, xx4002, gh)))
new_esEs26(xx3000, xx4000, app(ty_Ratio, bff)) → new_esEs16(xx3000, xx4000, bff)
new_esEs26(xx3000, xx4000, app(app(app(ty_@3, bgb), bgc), bgd)) → new_esEs18(xx3000, xx4000, bgb, bgc, bgd)
new_esEs26(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs26(xx3000, xx4000, app(app(ty_@2, bfc), bfd)) → new_esEs13(xx3000, xx4000, bfc, bfd)
new_esEs26(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs26(xx3000, xx4000, app(ty_Maybe, bfg)) → new_esEs17(xx3000, xx4000, bfg)
new_esEs26(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs26(xx3000, xx4000, app(ty_[], bfe)) → new_esEs14(xx3000, xx4000, bfe)
new_esEs26(xx3000, xx4000, app(app(ty_Either, bfh), bga)) → new_esEs6(xx3000, xx4000, bfh, bga)
new_esEs26(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs25(xx3001, xx4001, app(ty_[], bec)) → new_esEs14(xx3001, xx4001, bec)
new_esEs25(xx3001, xx4001, ty_Char) → new_esEs19(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(ty_Maybe, bee)) → new_esEs17(xx3001, xx4001, bee)
new_esEs25(xx3001, xx4001, ty_Bool) → new_esEs10(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(app(ty_Either, bef), beg)) → new_esEs6(xx3001, xx4001, bef, beg)
new_esEs25(xx3001, xx4001, app(ty_Ratio, bed)) → new_esEs16(xx3001, xx4001, bed)
new_esEs25(xx3001, xx4001, ty_Double) → new_esEs9(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_@0) → new_esEs7(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_Ordering) → new_esEs8(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(app(app(ty_@3, beh), bfa), bfb)) → new_esEs18(xx3001, xx4001, beh, bfa, bfb)
new_esEs25(xx3001, xx4001, ty_Float) → new_esEs11(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(app(ty_@2, bea), beb)) → new_esEs13(xx3001, xx4001, bea, beb)
new_esEs24(xx3002, xx4002, app(ty_Maybe, bdc)) → new_esEs17(xx3002, xx4002, bdc)
new_esEs24(xx3002, xx4002, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs18(xx3002, xx4002, bdf, bdg, bdh)
new_esEs24(xx3002, xx4002, ty_Double) → new_esEs9(xx3002, xx4002)
new_esEs24(xx3002, xx4002, app(app(ty_Either, bdd), bde)) → new_esEs6(xx3002, xx4002, bdd, bde)
new_esEs24(xx3002, xx4002, app(app(ty_@2, bcg), bch)) → new_esEs13(xx3002, xx4002, bcg, bch)
new_esEs24(xx3002, xx4002, app(ty_[], bda)) → new_esEs14(xx3002, xx4002, bda)
new_esEs24(xx3002, xx4002, ty_Integer) → new_esEs12(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_Int) → new_esEs15(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_Float) → new_esEs11(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_Char) → new_esEs19(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_Bool) → new_esEs10(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_@0) → new_esEs7(xx3002, xx4002)
new_esEs24(xx3002, xx4002, app(ty_Ratio, bdb)) → new_esEs16(xx3002, xx4002, bdb)
new_esEs24(xx3002, xx4002, ty_Ordering) → new_esEs8(xx3002, xx4002)
new_esEs19(Char(xx3000), Char(xx4000)) → new_primEqNat0(xx3000, xx4000)
new_esEs11(Float(xx3000, xx3001), Float(xx4000, xx4001)) → new_esEs15(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_sr(Pos(xx30010), Neg(xx40010)) → Neg(new_primMulNat0(xx30010, xx40010))
new_sr(Neg(xx30010), Pos(xx40010)) → Neg(new_primMulNat0(xx30010, xx40010))
new_sr(Neg(xx30010), Neg(xx40010)) → Pos(new_primMulNat0(xx30010, xx40010))
new_sr(Pos(xx30010), Pos(xx40010)) → Pos(new_primMulNat0(xx30010, xx40010))
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Succ(xx300100), Zero) → Zero
new_primMulNat0(Zero, Succ(xx400100)) → Zero
new_primMulNat0(Succ(xx300100), Succ(xx400100)) → new_primPlusNat1(new_primMulNat0(xx300100, Succ(xx400100)), xx400100)
new_primPlusNat1(Succ(xx370), xx400100) → Succ(Succ(new_primPlusNat0(xx370, xx400100)))
new_primPlusNat1(Zero, xx400100) → Succ(xx400100)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(xx3700), Succ(xx4001000)) → Succ(Succ(new_primPlusNat0(xx3700, xx4001000)))
new_primPlusNat0(Succ(xx3700), Zero) → Succ(xx3700)
new_primPlusNat0(Zero, Succ(xx4001000)) → Succ(xx4001000)
new_esEs14([], [], gc) → True
new_esEs14(:(xx3000, xx3001), :(xx4000, xx4001), gc) → new_asAs(new_esEs27(xx3000, xx4000, gc), new_esEs14(xx3001, xx4001, gc))
new_esEs14(:(xx3000, xx3001), [], gc) → False
new_esEs14([], :(xx4000, xx4001), gc) → False
new_esEs27(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs27(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(ty_Ratio, bgh)) → new_esEs16(xx3000, xx4000, bgh)
new_esEs27(xx3000, xx4000, app(ty_Maybe, bha)) → new_esEs17(xx3000, xx4000, bha)
new_esEs27(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(app(ty_Either, bhb), bhc)) → new_esEs6(xx3000, xx4000, bhb, bhc)
new_esEs27(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs27(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs27(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(app(ty_@2, bge), bgf)) → new_esEs13(xx3000, xx4000, bge, bgf)
new_esEs27(xx3000, xx4000, app(app(app(ty_@3, bhd), bhe), bhf)) → new_esEs18(xx3000, xx4000, bhd, bhe, bhf)
new_esEs27(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(ty_[], bgg)) → new_esEs14(xx3000, xx4000, bgg)
new_esEs27(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs13(@2(xx3000, xx3001), @2(xx4000, xx4001), ga, gb) → new_asAs(new_esEs21(xx3000, xx4000, ga), new_esEs20(xx3001, xx4001, gb))
new_esEs21(xx3000, xx4000, app(ty_Maybe, bag)) → new_esEs17(xx3000, xx4000, bag)
new_esEs21(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(app(ty_Either, bah), bba)) → new_esEs6(xx3000, xx4000, bah, bba)
new_esEs21(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs18(xx3000, xx4000, bbb, bbc, bbd)
new_esEs21(xx3000, xx4000, app(app(ty_@2, bac), bad)) → new_esEs13(xx3000, xx4000, bac, bad)
new_esEs21(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs21(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(ty_Ratio, baf)) → new_esEs16(xx3000, xx4000, baf)
new_esEs21(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs21(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(ty_[], bae)) → new_esEs14(xx3000, xx4000, bae)
new_esEs21(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs21(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs20(xx3001, xx4001, app(ty_Maybe, he)) → new_esEs17(xx3001, xx4001, he)
new_esEs20(xx3001, xx4001, ty_Bool) → new_esEs10(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_Char) → new_esEs19(xx3001, xx4001)
new_esEs20(xx3001, xx4001, app(ty_Ratio, hd)) → new_esEs16(xx3001, xx4001, hd)
new_esEs20(xx3001, xx4001, ty_Float) → new_esEs11(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_@0) → new_esEs7(xx3001, xx4001)
new_esEs20(xx3001, xx4001, app(app(ty_Either, hf), hg)) → new_esEs6(xx3001, xx4001, hf, hg)
new_esEs20(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_Ordering) → new_esEs8(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_Double) → new_esEs9(xx3001, xx4001)
new_esEs20(xx3001, xx4001, app(ty_[], hc)) → new_esEs14(xx3001, xx4001, hc)
new_esEs20(xx3001, xx4001, app(app(ty_@2, ha), hb)) → new_esEs13(xx3001, xx4001, ha, hb)
new_esEs20(xx3001, xx4001, app(app(app(ty_@3, hh), baa), bab)) → new_esEs18(xx3001, xx4001, hh, baa, bab)
new_esEs9(Double(xx3000, xx3001), Double(xx4000, xx4001)) → new_esEs15(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_esEs17(Just(xx3000), Just(xx4000), app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs18(xx3000, xx4000, bcd, bce, bcf)
new_esEs17(Just(xx3000), Just(xx4000), ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_Ratio, bbh)) → new_esEs16(xx3000, xx4000, bbh)
new_esEs17(Just(xx3000), Just(xx4000), ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), app(app(ty_@2, bbe), bbf)) → new_esEs13(xx3000, xx4000, bbe, bbf)
new_esEs17(Just(xx3000), Just(xx4000), ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs17(Nothing, Nothing, ge) → True
new_esEs17(Just(xx3000), Just(xx4000), ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs17(Just(xx3000), Nothing, ge) → False
new_esEs17(Nothing, Just(xx4000), ge) → False
new_esEs17(Just(xx3000), Just(xx4000), ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_[], bbg)) → new_esEs14(xx3000, xx4000, bbg)

The set Q consists of the following terms:

new_esEs6(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs27(x0, x1, ty_@0)
new_esEs17(Nothing, Nothing, x0)
new_esEs6(Right(x0), Right(x1), x2, ty_Char)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs7(@0, @0)
new_primMulNat0(Succ(x0), Zero)
new_esEs21(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Char)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs27(x0, x1, ty_Bool)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs4(x0, x1, ty_Double)
new_esEs18(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Char)
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Bool)
new_esEs6(Right(x0), Right(x1), x2, ty_Int)
new_primEqNat0(Succ(x0), Zero)
new_esEs22(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs14(:(x0, x1), [], x2)
new_esEs8(EQ, EQ)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Double)
new_esEs15(x0, x1)
new_esEs6(Right(x0), Right(x1), x2, ty_Double)
new_esEs21(x0, x1, ty_Ordering)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(x0, x1, ty_Int)
new_esEs17(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs5(x0, x1, ty_Float)
new_esEs11(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, ty_Float)
new_asAs(True, x0)
new_primMulNat0(Zero, Succ(x0))
new_esEs6(Left(x0), Left(x1), ty_Float, x2)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(Integer(x0), Integer(x1))
new_esEs24(x0, x1, ty_Double)
new_esEs8(GT, GT)
new_esEs25(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), ty_Integer, x2)
new_esEs6(Left(x0), Left(x1), ty_Int, x2)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs17(Just(x0), Just(x1), ty_Float)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, ty_@0)
new_esEs6(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs6(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs27(x0, x1, ty_Int)
new_esEs17(Just(x0), Just(x1), app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs8(LT, LT)
new_esEs27(x0, x1, ty_Char)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs17(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs14(:(x0, x1), :(x2, x3), x4)
new_esEs17(Just(x0), Just(x1), ty_Int)
new_esEs6(Left(x0), Left(x1), ty_@0, x2)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_sr(Neg(x0), Neg(x1))
new_esEs9(Double(x0, x1), Double(x2, x3))
new_primPlusNat0(Succ(x0), Zero)
new_esEs8(GT, EQ)
new_esEs8(EQ, GT)
new_esEs21(x0, x1, ty_Char)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs19(Char(x0), Char(x1))
new_esEs6(Right(x0), Right(x1), x2, ty_Integer)
new_esEs26(x0, x1, ty_Float)
new_esEs20(x0, x1, app(ty_[], x2))
new_sr(Pos(x0), Pos(x1))
new_esEs5(x0, x1, ty_Bool)
new_esEs6(Left(x0), Left(x1), ty_Char, x2)
new_esEs20(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Bool)
new_esEs8(LT, GT)
new_esEs8(GT, LT)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs27(x0, x1, ty_Double)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Integer)
new_esEs17(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs10(False, False)
new_esEs20(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Float)
new_esEs20(x0, x1, ty_Int)
new_primEqNat0(Zero, Zero)
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs25(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_@0)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, ty_Ordering)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_@0)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs26(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs17(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Right(x0), Right(x1), x2, ty_@0)
new_esEs6(Left(x0), Left(x1), ty_Double, x2)
new_esEs26(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_primMulNat0(Zero, Zero)
new_esEs26(x0, x1, ty_Ordering)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Ordering)
new_esEs6(Right(x0), Left(x1), x2, x3)
new_esEs6(Left(x0), Right(x1), x2, x3)
new_esEs17(Just(x0), Just(x1), ty_Char)
new_esEs23(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Char)
new_asAs(False, x0)
new_primPlusNat1(Succ(x0), x1)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Int)
new_esEs17(Just(x0), Nothing, x1)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs13(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs4(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Float)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs20(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs6(Left(x0), Left(x1), ty_Bool, x2)
new_esEs17(Just(x0), Just(x1), ty_@0)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs25(x0, x1, ty_Double)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs17(Just(x0), Just(x1), ty_Bool)
new_esEs17(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_@0)
new_esEs8(EQ, LT)
new_esEs8(LT, EQ)
new_esEs6(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs4(x0, x1, ty_Int)
new_esEs6(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs24(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Int)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs14([], :(x0, x1), x2)
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Zero, Succ(x0))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_Bool)
new_primPlusNat0(Zero, Zero)
new_esEs10(True, True)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Double)
new_esEs14([], [], x0)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs26(x0, x1, ty_Char)
new_esEs16(:%(x0, x1), :%(x2, x3), x4)
new_esEs21(x0, x1, ty_Bool)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, ty_Double)
new_esEs17(Nothing, Just(x0), x1)
new_esEs5(x0, x1, ty_Ordering)
new_esEs17(Just(x0), Just(x1), ty_Ordering)
new_esEs20(x0, x1, ty_Float)
new_primPlusNat0(Zero, Succ(x0))
new_esEs4(x0, x1, ty_Float)
new_esEs6(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Float)
new_esEs5(x0, x1, ty_Char)
new_esEs24(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Float)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs17(Just(x0), Just(x1), ty_Double)
new_primPlusNat1(Zero, x0)
new_esEs4(x0, x1, ty_Integer)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Int)
new_esEs5(x0, x1, ty_@0)
new_esEs17(Just(x0), Just(x1), ty_Integer)
new_esEs25(x0, x1, ty_@0)
new_esEs4(x0, x1, app(ty_[], x2))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_esEs5(x0, x1, app(ty_Maybe, x2))
new_esEs5(x0, x1, ty_Int)
new_esEs5(x0, x1, ty_Float)
new_esEs5(x0, x1, ty_Bool)
new_esEs5(x0, x1, ty_Integer)
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(x0, x1, ty_Double)
new_esEs5(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Char)
new_esEs5(x0, x1, ty_@0)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ DependencyGraphProof
                              ↳ AND
                                ↳ QDP
                                ↳ QDP
                                  ↳ UsableRulesProof
                                    ↳ QDP
                                      ↳ QReductionProof
                                        ↳ QDP
                                          ↳ QDPSizeChangeProof
                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs0(Left(xx300), :(Right(xx400), xx41), xx5, bc, bd) → new_psPs(xx300, False, xx41, xx5, bc, bd)
new_psPs(xx11, False, xx13, xx14, ba, bb) → new_psPs0(Left(xx11), xx13, xx14, ba, bb)
new_psPs0(Left(xx300), :(Left(xx400), xx41), xx5, bc, bd) → new_psPs(xx300, new_esEs4(xx300, xx400, bc), xx41, xx5, bc, bd)

The TRS R consists of the following rules:

new_esEs4(xx300, xx400, ty_Ordering) → new_esEs8(xx300, xx400)
new_esEs4(xx300, xx400, ty_Float) → new_esEs11(xx300, xx400)
new_esEs4(xx300, xx400, app(app(ty_@2, ga), gb)) → new_esEs13(xx300, xx400, ga, gb)
new_esEs4(xx300, xx400, app(ty_Maybe, ge)) → new_esEs17(xx300, xx400, ge)
new_esEs4(xx300, xx400, app(app(app(ty_@3, gf), gg), gh)) → new_esEs18(xx300, xx400, gf, gg, gh)
new_esEs4(xx300, xx400, ty_Char) → new_esEs19(xx300, xx400)
new_esEs4(xx300, xx400, ty_Bool) → new_esEs10(xx300, xx400)
new_esEs4(xx300, xx400, ty_Integer) → new_esEs12(xx300, xx400)
new_esEs4(xx300, xx400, ty_Double) → new_esEs9(xx300, xx400)
new_esEs4(xx300, xx400, app(ty_[], gc)) → new_esEs14(xx300, xx400, gc)
new_esEs4(xx300, xx400, app(app(ty_Either, dc), bg)) → new_esEs6(xx300, xx400, dc, bg)
new_esEs4(xx300, xx400, ty_Int) → new_esEs15(xx300, xx400)
new_esEs4(xx300, xx400, ty_@0) → new_esEs7(xx300, xx400)
new_esEs4(xx300, xx400, app(ty_Ratio, gd)) → new_esEs16(xx300, xx400, gd)
new_esEs16(:%(xx3000, xx3001), :%(xx4000, xx4001), gd) → new_asAs(new_esEs23(xx3000, xx4000, gd), new_esEs22(xx3001, xx4001, gd))
new_esEs23(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs23(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs22(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs22(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_asAs(False, xx36) → False
new_asAs(True, xx36) → xx36
new_esEs15(xx300, xx400) → new_primEqInt(xx300, xx400)
new_primEqInt(Neg(Succ(xx30000)), Pos(xx4000)) → False
new_primEqInt(Pos(Succ(xx30000)), Neg(xx4000)) → False
new_primEqInt(Pos(Zero), Neg(Succ(xx40000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(xx40000))) → False
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_primEqInt(Neg(Succ(xx30000)), Neg(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Succ(xx30000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(xx40000))) → False
new_primEqInt(Pos(Succ(xx30000)), Pos(Succ(xx40000))) → new_primEqNat0(xx30000, xx40000)
new_primEqInt(Pos(Zero), Pos(Succ(xx40000))) → False
new_primEqInt(Pos(Succ(xx30000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqNat0(Succ(xx30000), Zero) → False
new_primEqNat0(Zero, Succ(xx40000)) → False
new_primEqNat0(Zero, Zero) → True
new_primEqNat0(Succ(xx30000), Succ(xx40000)) → new_primEqNat0(xx30000, xx40000)
new_esEs12(Integer(xx3000), Integer(xx4000)) → new_primEqInt(xx3000, xx4000)
new_esEs7(@0, @0) → True
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), ty_@0, bg) → new_esEs7(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_Ratio, cc), bg) → new_esEs16(xx3000, xx4000, cc)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_Maybe, cd), bg) → new_esEs17(xx3000, xx4000, cd)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_Maybe, bca)) → new_esEs17(xx3000, xx4000, bca)
new_esEs17(Just(xx3000), Just(xx4000), app(app(ty_Either, bcb), bcc)) → new_esEs6(xx3000, xx4000, bcb, bcc)
new_esEs6(Left(xx3000), Left(xx4000), app(app(ty_Either, ce), cf), bg) → new_esEs6(xx3000, xx4000, ce, cf)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(ty_Either, ea), eb)) → new_esEs6(xx3000, xx4000, ea, eb)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_Maybe, dh)) → new_esEs17(xx3000, xx4000, dh)
new_esEs6(Left(xx3000), Left(xx4000), ty_Integer, bg) → new_esEs12(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), ty_Float, bg) → new_esEs11(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), ty_Char, bg) → new_esEs19(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_[], df)) → new_esEs14(xx3000, xx4000, df)
new_esEs6(Left(xx3000), Left(xx4000), ty_Ordering, bg) → new_esEs8(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(ty_@2, dd), de)) → new_esEs13(xx3000, xx4000, dd, de)
new_esEs6(Left(xx3000), Left(xx4000), ty_Double, bg) → new_esEs9(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs6(Left(xx3000), Right(xx4000), dc, bg) → False
new_esEs6(Right(xx3000), Left(xx4000), dc, bg) → False
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(app(app(ty_@3, cg), da), db), bg) → new_esEs18(xx3000, xx4000, cg, da, db)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(ty_Ratio, dg)) → new_esEs16(xx3000, xx4000, dg)
new_esEs6(Left(xx3000), Left(xx4000), app(app(ty_@2, bh), ca), bg) → new_esEs13(xx3000, xx4000, bh, ca)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), ty_Int, bg) → new_esEs15(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs6(Left(xx3000), Left(xx4000), app(ty_[], cb), bg) → new_esEs14(xx3000, xx4000, cb)
new_esEs6(Right(xx3000), Right(xx4000), dc, app(app(app(ty_@3, ec), ed), ee)) → new_esEs18(xx3000, xx4000, ec, ed, ee)
new_esEs6(Left(xx3000), Left(xx4000), ty_Bool, bg) → new_esEs10(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs6(Right(xx3000), Right(xx4000), dc, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs8(GT, EQ) → False
new_esEs8(EQ, GT) → False
new_esEs8(LT, LT) → True
new_esEs8(GT, GT) → True
new_esEs8(GT, LT) → False
new_esEs8(LT, GT) → False
new_esEs8(EQ, EQ) → True
new_esEs8(EQ, LT) → False
new_esEs8(LT, EQ) → False
new_esEs10(True, True) → True
new_esEs10(False, False) → True
new_esEs10(False, True) → False
new_esEs10(True, False) → False
new_esEs18(@3(xx3000, xx3001, xx3002), @3(xx4000, xx4001, xx4002), gf, gg, gh) → new_asAs(new_esEs26(xx3000, xx4000, gf), new_asAs(new_esEs25(xx3001, xx4001, gg), new_esEs24(xx3002, xx4002, gh)))
new_esEs26(xx3000, xx4000, app(ty_Ratio, bff)) → new_esEs16(xx3000, xx4000, bff)
new_esEs26(xx3000, xx4000, app(app(app(ty_@3, bgb), bgc), bgd)) → new_esEs18(xx3000, xx4000, bgb, bgc, bgd)
new_esEs26(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs26(xx3000, xx4000, app(app(ty_@2, bfc), bfd)) → new_esEs13(xx3000, xx4000, bfc, bfd)
new_esEs26(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs26(xx3000, xx4000, app(ty_Maybe, bfg)) → new_esEs17(xx3000, xx4000, bfg)
new_esEs26(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs26(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs26(xx3000, xx4000, app(ty_[], bfe)) → new_esEs14(xx3000, xx4000, bfe)
new_esEs26(xx3000, xx4000, app(app(ty_Either, bfh), bga)) → new_esEs6(xx3000, xx4000, bfh, bga)
new_esEs26(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs25(xx3001, xx4001, app(ty_[], bec)) → new_esEs14(xx3001, xx4001, bec)
new_esEs25(xx3001, xx4001, ty_Char) → new_esEs19(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(ty_Maybe, bee)) → new_esEs17(xx3001, xx4001, bee)
new_esEs25(xx3001, xx4001, ty_Bool) → new_esEs10(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(app(ty_Either, bef), beg)) → new_esEs6(xx3001, xx4001, bef, beg)
new_esEs25(xx3001, xx4001, app(ty_Ratio, bed)) → new_esEs16(xx3001, xx4001, bed)
new_esEs25(xx3001, xx4001, ty_Double) → new_esEs9(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_@0) → new_esEs7(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_Ordering) → new_esEs8(xx3001, xx4001)
new_esEs25(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(app(app(ty_@3, beh), bfa), bfb)) → new_esEs18(xx3001, xx4001, beh, bfa, bfb)
new_esEs25(xx3001, xx4001, ty_Float) → new_esEs11(xx3001, xx4001)
new_esEs25(xx3001, xx4001, app(app(ty_@2, bea), beb)) → new_esEs13(xx3001, xx4001, bea, beb)
new_esEs24(xx3002, xx4002, app(ty_Maybe, bdc)) → new_esEs17(xx3002, xx4002, bdc)
new_esEs24(xx3002, xx4002, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs18(xx3002, xx4002, bdf, bdg, bdh)
new_esEs24(xx3002, xx4002, ty_Double) → new_esEs9(xx3002, xx4002)
new_esEs24(xx3002, xx4002, app(app(ty_Either, bdd), bde)) → new_esEs6(xx3002, xx4002, bdd, bde)
new_esEs24(xx3002, xx4002, app(app(ty_@2, bcg), bch)) → new_esEs13(xx3002, xx4002, bcg, bch)
new_esEs24(xx3002, xx4002, app(ty_[], bda)) → new_esEs14(xx3002, xx4002, bda)
new_esEs24(xx3002, xx4002, ty_Integer) → new_esEs12(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_Int) → new_esEs15(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_Float) → new_esEs11(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_Char) → new_esEs19(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_Bool) → new_esEs10(xx3002, xx4002)
new_esEs24(xx3002, xx4002, ty_@0) → new_esEs7(xx3002, xx4002)
new_esEs24(xx3002, xx4002, app(ty_Ratio, bdb)) → new_esEs16(xx3002, xx4002, bdb)
new_esEs24(xx3002, xx4002, ty_Ordering) → new_esEs8(xx3002, xx4002)
new_esEs19(Char(xx3000), Char(xx4000)) → new_primEqNat0(xx3000, xx4000)
new_esEs11(Float(xx3000, xx3001), Float(xx4000, xx4001)) → new_esEs15(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_sr(Pos(xx30010), Neg(xx40010)) → Neg(new_primMulNat0(xx30010, xx40010))
new_sr(Neg(xx30010), Pos(xx40010)) → Neg(new_primMulNat0(xx30010, xx40010))
new_sr(Neg(xx30010), Neg(xx40010)) → Pos(new_primMulNat0(xx30010, xx40010))
new_sr(Pos(xx30010), Pos(xx40010)) → Pos(new_primMulNat0(xx30010, xx40010))
new_primMulNat0(Zero, Zero) → Zero
new_primMulNat0(Succ(xx300100), Zero) → Zero
new_primMulNat0(Zero, Succ(xx400100)) → Zero
new_primMulNat0(Succ(xx300100), Succ(xx400100)) → new_primPlusNat1(new_primMulNat0(xx300100, Succ(xx400100)), xx400100)
new_primPlusNat1(Succ(xx370), xx400100) → Succ(Succ(new_primPlusNat0(xx370, xx400100)))
new_primPlusNat1(Zero, xx400100) → Succ(xx400100)
new_primPlusNat0(Zero, Zero) → Zero
new_primPlusNat0(Succ(xx3700), Succ(xx4001000)) → Succ(Succ(new_primPlusNat0(xx3700, xx4001000)))
new_primPlusNat0(Succ(xx3700), Zero) → Succ(xx3700)
new_primPlusNat0(Zero, Succ(xx4001000)) → Succ(xx4001000)
new_esEs14([], [], gc) → True
new_esEs14(:(xx3000, xx3001), :(xx4000, xx4001), gc) → new_asAs(new_esEs27(xx3000, xx4000, gc), new_esEs14(xx3001, xx4001, gc))
new_esEs14(:(xx3000, xx3001), [], gc) → False
new_esEs14([], :(xx4000, xx4001), gc) → False
new_esEs27(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs27(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(ty_Ratio, bgh)) → new_esEs16(xx3000, xx4000, bgh)
new_esEs27(xx3000, xx4000, app(ty_Maybe, bha)) → new_esEs17(xx3000, xx4000, bha)
new_esEs27(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(app(ty_Either, bhb), bhc)) → new_esEs6(xx3000, xx4000, bhb, bhc)
new_esEs27(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs27(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs27(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(app(ty_@2, bge), bgf)) → new_esEs13(xx3000, xx4000, bge, bgf)
new_esEs27(xx3000, xx4000, app(app(app(ty_@3, bhd), bhe), bhf)) → new_esEs18(xx3000, xx4000, bhd, bhe, bhf)
new_esEs27(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs27(xx3000, xx4000, app(ty_[], bgg)) → new_esEs14(xx3000, xx4000, bgg)
new_esEs27(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs13(@2(xx3000, xx3001), @2(xx4000, xx4001), ga, gb) → new_asAs(new_esEs21(xx3000, xx4000, ga), new_esEs20(xx3001, xx4001, gb))
new_esEs21(xx3000, xx4000, app(ty_Maybe, bag)) → new_esEs17(xx3000, xx4000, bag)
new_esEs21(xx3000, xx4000, ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(app(ty_Either, bah), bba)) → new_esEs6(xx3000, xx4000, bah, bba)
new_esEs21(xx3000, xx4000, ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs18(xx3000, xx4000, bbb, bbc, bbd)
new_esEs21(xx3000, xx4000, app(app(ty_@2, bac), bad)) → new_esEs13(xx3000, xx4000, bac, bad)
new_esEs21(xx3000, xx4000, ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs21(xx3000, xx4000, ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(ty_Ratio, baf)) → new_esEs16(xx3000, xx4000, baf)
new_esEs21(xx3000, xx4000, ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs21(xx3000, xx4000, ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs21(xx3000, xx4000, app(ty_[], bae)) → new_esEs14(xx3000, xx4000, bae)
new_esEs21(xx3000, xx4000, ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs21(xx3000, xx4000, ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs20(xx3001, xx4001, app(ty_Maybe, he)) → new_esEs17(xx3001, xx4001, he)
new_esEs20(xx3001, xx4001, ty_Bool) → new_esEs10(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_Char) → new_esEs19(xx3001, xx4001)
new_esEs20(xx3001, xx4001, app(ty_Ratio, hd)) → new_esEs16(xx3001, xx4001, hd)
new_esEs20(xx3001, xx4001, ty_Float) → new_esEs11(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_@0) → new_esEs7(xx3001, xx4001)
new_esEs20(xx3001, xx4001, app(app(ty_Either, hf), hg)) → new_esEs6(xx3001, xx4001, hf, hg)
new_esEs20(xx3001, xx4001, ty_Integer) → new_esEs12(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_Ordering) → new_esEs8(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_Int) → new_esEs15(xx3001, xx4001)
new_esEs20(xx3001, xx4001, ty_Double) → new_esEs9(xx3001, xx4001)
new_esEs20(xx3001, xx4001, app(ty_[], hc)) → new_esEs14(xx3001, xx4001, hc)
new_esEs20(xx3001, xx4001, app(app(ty_@2, ha), hb)) → new_esEs13(xx3001, xx4001, ha, hb)
new_esEs20(xx3001, xx4001, app(app(app(ty_@3, hh), baa), bab)) → new_esEs18(xx3001, xx4001, hh, baa, bab)
new_esEs9(Double(xx3000, xx3001), Double(xx4000, xx4001)) → new_esEs15(new_sr(xx3000, xx4000), new_sr(xx3001, xx4001))
new_esEs17(Just(xx3000), Just(xx4000), app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs18(xx3000, xx4000, bcd, bce, bcf)
new_esEs17(Just(xx3000), Just(xx4000), ty_Double) → new_esEs9(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), ty_Float) → new_esEs11(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_Ratio, bbh)) → new_esEs16(xx3000, xx4000, bbh)
new_esEs17(Just(xx3000), Just(xx4000), ty_Char) → new_esEs19(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), ty_@0) → new_esEs7(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), app(app(ty_@2, bbe), bbf)) → new_esEs13(xx3000, xx4000, bbe, bbf)
new_esEs17(Just(xx3000), Just(xx4000), ty_Integer) → new_esEs12(xx3000, xx4000)
new_esEs17(Nothing, Nothing, ge) → True
new_esEs17(Just(xx3000), Just(xx4000), ty_Int) → new_esEs15(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), ty_Ordering) → new_esEs8(xx3000, xx4000)
new_esEs17(Just(xx3000), Nothing, ge) → False
new_esEs17(Nothing, Just(xx4000), ge) → False
new_esEs17(Just(xx3000), Just(xx4000), ty_Bool) → new_esEs10(xx3000, xx4000)
new_esEs17(Just(xx3000), Just(xx4000), app(ty_[], bbg)) → new_esEs14(xx3000, xx4000, bbg)

The set Q consists of the following terms:

new_esEs6(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs27(x0, x1, ty_@0)
new_esEs17(Nothing, Nothing, x0)
new_esEs6(Right(x0), Right(x1), x2, ty_Char)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs7(@0, @0)
new_primMulNat0(Succ(x0), Zero)
new_esEs21(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_Char)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs27(x0, x1, ty_Bool)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs4(x0, x1, ty_Double)
new_esEs18(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Char)
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Bool)
new_esEs6(Right(x0), Right(x1), x2, ty_Int)
new_primEqNat0(Succ(x0), Zero)
new_esEs22(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs14(:(x0, x1), [], x2)
new_esEs8(EQ, EQ)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Double)
new_esEs15(x0, x1)
new_esEs6(Right(x0), Right(x1), x2, ty_Double)
new_esEs21(x0, x1, ty_Ordering)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_primPlusNat0(Succ(x0), Succ(x1))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs17(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs11(Float(x0, x1), Float(x2, x3))
new_esEs27(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs27(x0, x1, ty_Float)
new_asAs(True, x0)
new_primMulNat0(Zero, Succ(x0))
new_esEs6(Left(x0), Left(x1), ty_Float, x2)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(Integer(x0), Integer(x1))
new_esEs24(x0, x1, ty_Double)
new_esEs8(GT, GT)
new_esEs25(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), ty_Integer, x2)
new_esEs6(Left(x0), Left(x1), ty_Int, x2)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs17(Just(x0), Just(x1), ty_Float)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, ty_@0)
new_esEs6(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs6(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs27(x0, x1, ty_Int)
new_esEs17(Just(x0), Just(x1), app(ty_[], x2))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Bool)
new_esEs6(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs8(LT, LT)
new_esEs27(x0, x1, ty_Char)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs17(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs14(:(x0, x1), :(x2, x3), x4)
new_esEs17(Just(x0), Just(x1), ty_Int)
new_esEs6(Left(x0), Left(x1), ty_@0, x2)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_sr(Neg(x0), Neg(x1))
new_esEs9(Double(x0, x1), Double(x2, x3))
new_primPlusNat0(Succ(x0), Zero)
new_esEs8(GT, EQ)
new_esEs8(EQ, GT)
new_esEs21(x0, x1, ty_Char)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs19(Char(x0), Char(x1))
new_esEs6(Right(x0), Right(x1), x2, ty_Integer)
new_esEs26(x0, x1, ty_Float)
new_esEs20(x0, x1, app(ty_[], x2))
new_sr(Pos(x0), Pos(x1))
new_esEs6(Left(x0), Left(x1), ty_Char, x2)
new_esEs20(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Bool)
new_esEs8(LT, GT)
new_esEs8(GT, LT)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs27(x0, x1, ty_Double)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs10(False, False)
new_esEs20(x0, x1, ty_@0)
new_esEs24(x0, x1, ty_Float)
new_esEs20(x0, x1, ty_Int)
new_primEqNat0(Zero, Zero)
new_esEs6(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs25(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_@0)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Ordering)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_@0)
new_esEs6(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs26(x0, x1, ty_Integer)
new_esEs6(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs17(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs6(Right(x0), Right(x1), x2, ty_@0)
new_esEs6(Left(x0), Left(x1), ty_Double, x2)
new_esEs26(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_primMulNat0(Zero, Zero)
new_esEs26(x0, x1, ty_Ordering)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Ordering)
new_esEs6(Right(x0), Left(x1), x2, x3)
new_esEs6(Left(x0), Right(x1), x2, x3)
new_esEs17(Just(x0), Just(x1), ty_Char)
new_esEs23(x0, x1, ty_Integer)
new_esEs4(x0, x1, ty_Char)
new_asAs(False, x0)
new_primPlusNat1(Succ(x0), x1)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Int)
new_esEs17(Just(x0), Nothing, x1)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs13(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs4(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Float)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs20(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs6(Left(x0), Left(x1), ty_Bool, x2)
new_esEs17(Just(x0), Just(x1), ty_@0)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs25(x0, x1, ty_Double)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs17(Just(x0), Just(x1), ty_Bool)
new_esEs17(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_@0)
new_esEs8(EQ, LT)
new_esEs8(LT, EQ)
new_esEs6(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs4(x0, x1, ty_Int)
new_esEs6(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs24(x0, x1, ty_Ordering)
new_esEs24(x0, x1, ty_Int)
new_esEs14([], :(x0, x1), x2)
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_primEqNat0(Zero, Succ(x0))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_Bool)
new_primPlusNat0(Zero, Zero)
new_esEs10(True, True)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Double)
new_esEs14([], [], x0)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs26(x0, x1, ty_Char)
new_esEs16(:%(x0, x1), :%(x2, x3), x4)
new_esEs21(x0, x1, ty_Bool)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs17(Nothing, Just(x0), x1)
new_esEs17(Just(x0), Just(x1), ty_Ordering)
new_esEs20(x0, x1, ty_Float)
new_primPlusNat0(Zero, Succ(x0))
new_esEs4(x0, x1, ty_Float)
new_esEs6(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs6(Right(x0), Right(x1), x2, ty_Float)
new_esEs24(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Float)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs17(Just(x0), Just(x1), ty_Double)
new_primPlusNat1(Zero, x0)
new_esEs4(x0, x1, ty_Integer)
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs26(x0, x1, ty_Int)
new_esEs17(Just(x0), Just(x1), ty_Integer)
new_esEs25(x0, x1, ty_@0)
new_esEs4(x0, x1, app(ty_[], x2))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ Narrow
                        ↳ AND
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                          ↳ QDP
                            ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldr(xx4, :(xx30, xx31), ba, bb) → new_foldr(xx4, xx31, ba, bb)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: